Exercises for math student formalized on computers

We present here a list of exercices that can easely be formilized on computers and have been used to teach mathematics to students. We give the prover used, but these examples are so simple that they should be usable with almost any prover (admitting classical logic).

If you know some other exercices, send them to me by email, I will be pleased to add them here! It would be nice if you could send them in HTML respecting the same layout (no necessarily the same syntax).

We recall PhoX syntax :

• /\: for all
• \/: exists
• &: conjunction
• or: disjunction
• ->: implication
• <->: equivalence
• P x may be read x belongs to P in some cases because we use predicates do encode sets.

Analysis

Continuous functions and connected sets (PhoX):

This exercise relates two definitions of continous functions and shows that the image of a connected set by a continuous function is connected. It is surprising that no hypothesis are needed. Note: for the converse of the implication of the first statement, one needs the triangular inequality.

Statements:

• /\f (continue1 f -> continue2 f)
• /\f (continue2 f -> /\ A (connexe A -> connexe (image f A)))

Hypothesis:

• None !

Definitions:

• image f A y = \/ x ((A x) & (f x) = y)
• inverse f A x = (A (f x))
• intervide U V = ~ \/ x ((U x) & (V x))
• Union A B x = (A x) or (B x)
• inclus A B = /\ x ((A x) -> (B x))
• ouvert O =/\ x (O x -> \/a > 0 /\y (d x y < a -> O y))
• connexe A = /\ U, V (ouvert U -> ouvert V -> (inclus A (union U V)) -> (intervide U V) -> (inclus A U) or (inclus A V))
• continue1 f = /\ x /\e > 0 \/a > 0 /\ y (d x y < a -> d (f x) (f y) < e)
• continue2 f = /\ U ((ouvert U) -> (ouvert (inverse f U)))

Union and closure (PhoX):

The union of the closure is the closure of the union.

Statement:

• /\A /\B /\x (Union (Adh A) (Adh B) x <-> Adh (Union A B) x)

Hypothesis:

• /\e_1 >0 /\e_2 >0 \/e >0 (e < e_1 & e < e_2)
• /\x,y,z (x < y -> y < z -> x < z)

Definitions:

• Union A B x = (A x) or (B x)
  
• Adh A x = /\e > 0 \/y (A y & d x y < e)

Algebra

Injections and disjoint support (PhoX):

Two injections with disjoint support commute.

Statement:

• /\h,g (injective h & injective g & /\x (h x = x or g x = x) -> /\x (h (g x)) = (g (h x)))

Hypothesis:

• None !

Definitions:

• injective f = /\x,y (f x = f y -> x = y)