>PhoX> Sort real. Sort real defined >PhoX> Cst Infix[5.0] x "<" y : real real prop. $< : real real prop >PhoX> def Infix[5.0] x ">" y = y < x. $> = \x,y (y < x) : real real prop >PhoX> Cst d : real real real. d : real real real >PhoX> Cst R0 : real. R0 : real >PhoX> def image f A y = x ((A x) (f x) = y). image = \f,A,y x:A f x = y : ('b 'a) ( 'b prop) 'a prop >PhoX> def inverse f A x = (A (f x)). inverse = \f,A,x (A (f x)) : ('b 'c) ('c 'a) 'b 'a >PhoX> def intervide U V = x ((U x) (V x)). intervide = \U,V x:U V x : ('a prop) ( 'a prop) prop >PhoX> def union U V x = (U x) (V x). union = \U,V,x (U x V x) : ('a prop) ('a prop) 'a prop >PhoX> def inclus A B = x ((A x) (B x)). inclus = \A,B x:A B x : ('a prop) ('a prop) prop >PhoX> def ouvert O = x (O x a > R0 y (d x y < a O y)). ouvert = \O x:O a > R0 y (d x y < a O y) : (real prop) prop >PhoX> def connexe A = U, V (ouvert U ouvert V (inclus A (union U >PhoX> V)) (intervide U V) (inclus A U) (inclus A V)). connexe = \A U,V (ouvert U ouvert V inclus A (union U V) intervide U V inclus A U inclus A V) : (real prop) prop >PhoX> def continue1 f = x e > R0 a > R0 y (d x y < a d (f >PhoX> x) (f y) < e). continue1 = \f x,e (e > R0 a > R0 y (d x y < a d (f x) (f y) < e)) : (real real) prop >PhoX> def continue2 f = U ((ouvert U) (ouvert (inverse f U))). continue2 = \f U:ouvert ouvert (inverse f U) : (real real) prop >PhoX> lemma lem1 f (continue1 f continue2 f). Here is the goal: goal 1/1 f:continue1 continue2 f %PhoX% intros. 1 goal created. goal 1/1 H := continue1 f continue2 f %PhoX% intros. 1 goal created. goal 1/1 H := continue1 f H0 := ouvert U ouvert (inverse f U) %PhoX% intros. 1 goal created. goal 1/1 H := continue1 f H0 := ouvert U H1 := inverse f U x a > R0 y (d x y < a inverse f U y) %PhoX% unfold_hyp H1 inverse. 1 goal created. goal 1/1 H := continue1 f H0 := ouvert U H1 := U (f x) a > R0 y (d x y < a inverse f U y) %PhoX% unfold_hyp H0 ouvert. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a > R0 y (d x0 y < a U y) a > R0 y (d x y < a inverse f U y) %PhoX% apply H0 with H1. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a > R0 y (d x0 y < a U y) G := a > R0 y (d (f x) y < a U y) a > R0 y (d x y < a inverse f U y) %PhoX% lefts G $ $. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a0 > R0 y (d x0 y < a0 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) a0 > R0 y (d x y < a0 inverse f U y) %PhoX% apply H with H2. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a0 > R0 y (d x0 y < a0 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) G := a0 > R0 y (d ?1 y < a0 d (f ?1) (f y) < a) a0 > R0 y (d x y < a0 inverse f U y) %PhoX% lefts G $ $. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y (d x0 y < a1 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) H4 := a0 > R0 H5 := y (d ?1 y < a0 d (f ?1) (f y) < a) a1 > R0 y (d x y < a1 inverse f U y) %PhoX% intros. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y (d x0 y < a1 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) H4 := a0 > R0 H5 := y (d ?1 y < a0 d (f ?1) (f y) < a) ?2 > R0 y (d x y < ?2 inverse f U y) %PhoX% intro. 2 goals created. goal 2/2 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y (d x0 y < a1 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) H4 := a0 > R0 H5 := y (d ?1 y < a0 d (f ?1) (f y) < a) y (d x y < ?2 inverse f U y) goal 1/2 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y (d x0 y < a1 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) H4 := a0 > R0 H5 := y (d ?1 y < a0 d (f ?1) (f y) < a) ?2 > R0 %PhoX% axiom H4. 0 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y (d x0 y < a1 U y) H2 := a > R0 H3 := y (d (f x) y < a U y) H4 := a0 > R0 H5 := y (d ?1 y < a0 d (f ?1) (f y) < a) y (d x y < a0 inverse f U y) %PhoX% intros. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y0 (d x0 y0 < a1 U y0) H2 := a > R0 H3 := y0 (d (f x) y0 < a U y0) H4 := a0 > R0 H5 := y0 (d ?1 y0 < a0 d (f ?1) (f y0) < a) H6 := d x y < a0 inverse f U y %PhoX% elim H3. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y0 (d x0 y0 < a1 U y0) H2 := a > R0 H3 := y0 (d (f x) y0 < a U y0) H4 := a0 > R0 H5 := y0 (d ?1 y0 < a0 d (f ?1) (f y0) < a) H6 := d x y < a0 d (f x) (f y) < a %PhoX% elim H5. 1 goal created. goal 1/1 H := continue1 f H1 := U (f x) H0 := x0:U a1 > R0 y0 (d x0 y0 < a1 U y0) H2 := a > R0 H3 := y0 (d (f x) y0 < a U y0) H4 := a0 > R0 H5 := y0 (d x y0 < a0 d (f x) (f y0) < a) H6 := d x y < a0 d x y < a0 %PhoX% axiom H6. 0 goal created. %PhoX% save lem1. Building proof .... Typing proof .... Verifying proof .... Saving proof .... lem1 = f:continue1 continue2 f : theorem >PhoX> lemma lem2 f (continue2 f A (connexe A connexe (image f A))). Here is the goal: goal 1/1 f:continue2 A:connexe connexe (image f A) %PhoX% intros. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A connexe (image f A) %PhoX% intros. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V inclus (image f A) U inclus (image f A) V %PhoX% by_absurd. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) inclus (image f A) U inclus (image f A) V %PhoX% elim False. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) False %PhoX% local U' = inverse f U. U' = inverse f U : real prop 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) False %PhoX% local V' = inverse f V. V' = inverse f V : real prop 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) False %PhoX% prove ouvert U'. 2 goals created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) ouvert U' %PhoX% elim H. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) ouvert U %PhoX% axiom H1. 0 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' False %PhoX% prove ouvert V'. 2 goals created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' ouvert V' %PhoX% elim H. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' ouvert V %PhoX% axiom H2. 0 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' False %PhoX% prove inclus A (union U' V'). 2 goals created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' inclus A (union U' V') %PhoX% intros. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x union U' V' x %PhoX% elim H3. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x image f A (f x) %PhoX% intros. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x A ?1 f ?1 = f x %PhoX% intro. 2 goals created. goal 2/3 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x f ?1 = f x goal 1/3 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x A ?1 %PhoX% axiom H6. 0 goal created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' H6 := A x f x = f x %PhoX% intro. 0 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') False %PhoX% prove intervide U' V'. 2 goals created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') intervide U' V' %PhoX% intros. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') H6 := x:U' V' x False %PhoX% elim H4. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') H6 := x:U' V' x x:U V x %PhoX% left H6. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') H6 := U' x V' x x0:U V x0 %PhoX% intros. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') H6 := U' x V' x U ?2 V ?2 %PhoX% axiom H6. 0 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' False %PhoX% apply H0 with G and G0 and G1 and G2. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V H5 := (inclus (image f A) U inclus (image f A) V) G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' G3 := inclus A U' inclus A V' False %PhoX% rewrite_hyp H5 disjunction.demorgan. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' G3 := inclus A U' inclus A V' H5 := inclus (image f A) U inclus (image f A) V False %PhoX% left H5. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' G3 := inclus A U' inclus A V' H5 := inclus (image f A) U H6 := inclus (image f A) V False %PhoX% left G3. 2 goals created. goal 2/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' False goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A V' False %PhoX% elim H6. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A V' inclus (image f A) V %PhoX% intros. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A V' H8 := image f A x V x %PhoX% left H8. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A V' H8 := A x0 f x0 = x V x %PhoX% elim H7. 1 goal created. goal 1/2 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A V' H8 := A x0 f x0 = x A x0 %PhoX% elim H8. 0 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' False %PhoX% elim H5. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' inclus (image f A) U %PhoX% intros. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' H8 := image f A x U x %PhoX% left H8. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' H8 := A x0 f x0 = x U x %PhoX% elim H7. 1 goal created. goal 1/1 H := continue2 f H0 := connexe A H1 := ouvert U H2 := ouvert V H3 := inclus (image f A) (union U V) H4 := intervide U V G := ouvert U' G0 := ouvert V' G1 := inclus A (union U' V') G2 := intervide U' V' H5 := inclus (image f A) U H6 := inclus (image f A) V H7 := inclus A U' H8 := A x0 f x0 = x A x0 %PhoX% elim H8. 0 goal created. %PhoX% save lem2. Building proof .... Typing proof .... Verifying proof .... Saving proof .... lem2 = f:continue2 A:connexe connexe (image f A) : theorem >PhoX> goal f (continue1 f A (connexe A connexe (image f A))). Here is the goal: goal 1/1 f:continue1 A:connexe connexe (image f A) %PhoX% intro 2. 1 goal created. goal 1/1 H := continue1 f A:connexe connexe (image f A) %PhoX% elim lem2. 1 goal created. goal 1/1 H := continue1 f continue2 f %PhoX% elim lem1. 1 goal created. goal 1/1 H := continue1 f continue1 f %PhoX% axiom H. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = f:continue1 A:connexe connexe (image f A) : theorem bye