Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export notation. Module Topology_notation. Export Function. Export Notation. Definition Opens := (o_(p_(e_(n_(s_(DOT 0)))))). Definition caseOpens a (b : notn) op := match op return (atof op) with (o_(p_(e_(n_(s_(DOT 0)))))) => a | z => (b z) end. Definition Distance := (d_(i_(s_(t_(n_(DOT 2)))))). Definition caseDistance a (b : notn) op := match op return (atof op) with (d_(i_(s_(t_(n_(DOT 2)))))) => a | z => (b z) end. Definition Structure := (s_(t_(r_(u_(c_(t_(DOT 0))))))). Definition caseStructure a (b : notn) op := match op return (atof op) with (s_(t_(r_(u_(c_(t_(DOT 0))))))) => a | z => (b z) end. Definition opens (x : E) := extra x Opens. Definition distance' (x a b : E) := extra x Distance a b. Definition structure (x : E) := extra x Structure. (*** topological and possibly metric spaces, maybe with other structure put into the Structure variable ***) Definition distance (a x y : E) := mask (A (inc x (U a)) (inc y (U a))) (distance' a x y). Definition is_open (a u : E) := A (sub u (U a)) (inc u (opens a)). Lemma distance_prime : forall a x y : E, inc x (U a) -> inc y (U a) -> distance a x y = distance' a x y. ir. uf distance; ap mask_in. ee; am. Qed. Lemma distance_eq : forall a b : E, U a = U b -> (forall x y : E, inc x (U a) -> inc y (U a) -> distance a x y = distance b x y) -> distance a = distance b. ir. ap arrow_extensionality; intro x. ap arrow_extensionality; intro y. apply by_cases with (A (inc x (U a)) (inc y (U a))); ir. ee; ap H0; am. uf distance. rw mask_out. rw mask_out; tv. wr H. am. am. Qed. Section def. Variables x v_opens v_structure : E. Variable v_distance : E2. Definition create_obj op := caseUnderlying x ( caseOpens v_opens ( caseDistance v_distance ( caseStructure v_structure da))) op. Definition create_ens := createN create_obj. Lemma related_obj : forall a : E, inc a x -> related create_obj a. ir. sub_relate Underlying. am. Qed. Lemma U_rw : U create_ens = x. ir; uf U; uf create_ens. notatac1; am. Qed. Lemma opens_rw : opens create_ens = v_opens. ir; uf opens; uf create_ens. notatac1; am. Qed. Lemma structure_rw : structure create_ens = v_structure. ir; uf structure; uf create_ens. notatac1; am. Qed. Lemma distance_rw : forall a b : E, inc a x -> inc b x -> distance create_ens a b = v_distance a b. ir. rw distance_prime. uf distance'; uf create_ens. notatac1; ap related_obj; am. rw U_rw. am. rw U_rw. am. Qed. End def. Definition like (a : E) := create_ens (U a) (opens a) (structure a) (distance a) = a. Definition same (a b : E) := A (U a = U b) (A (opens a = opens b) (A (is_open a = is_open b) (A (structure a = structure b) (distance a = distance b)))). Lemma show_same : forall a b : E, U a = U b -> opens a = opens b -> structure a = structure b -> (forall x y : E, inc x (U a) -> inc y (U a) -> distance a x y = distance b x y) -> same a b. ir. uhg; dj. am. am. ap arrow_extensionality; ir. ap iff_eq; ir. uhg; uh H5; ee. wr H3; am. wr H4; am. uhg; uh H5; ee. rw H3; am. rw H4; am. am. ap distance_eq; am. Qed. Lemma like_same_eq : forall a b : E, like a -> like b -> same a b -> a = b. ir. uh H. uh H0. wr H. wr H0. uh H1; ee. rw H1. rw H2. rw H4. rw H5. tv. Qed. Lemma create_same : forall a : E, same a (create_ens (U a) (opens a) (structure a) (distance a)). ir. ap show_same; ir. rw U_rw. tv. rw opens_rw; tv. rw structure_rw; tv. rw distance_rw. tv. am. am. Qed. Lemma create_like : forall a : E, like (create_ens (U a) (opens a) (structure a) (distance a)). ir. set (K := create_ens (U a) (opens a) (structure a) (distance a)) in *. uhg. assert (same a K). uf K; ap create_same. uh H; ee. wr H; wr H0; wr H2; wr H3. tv. Qed. End Topology_notation. Module Topology. Export Topology_notation. Definition property x t := sub t (powerset x) & inc x t & inc emptyset t & (forall z, sub z t -> inc (union z) t) & (forall u v, inc u t -> inc v t -> inc (intersection2 u v) t). Definition axioms t := sub (opens t) (powerset (U t)) & is_open t (U t)& is_open t emptyset & (forall z, (forall u, inc u z -> is_open t u) -> is_open t (union z)) & (forall u v, is_open t u -> is_open t v -> is_open t (intersection2 u v)). Lemma create_axioms : forall x v_opens v_structure v_distance, property x v_opens -> axioms (create_ens x v_opens v_structure v_distance). Proof. ir. set (a:= create_ens x v_opens v_structure v_distance). assert (lem1:forall u, is_open a u = inc u v_opens). ir. ap iff_eq. ir. uh H0; ee. ufi a H1; rwi opens_rw H1; am. ir. uhg; ir. ee. wr powerset_inc_rw. uh H. ee. uf a; rw U_rw. ap H. am. uf a; rw opens_rw; am. uhg; dj. uf a; rw opens_rw; rw U_rw; lu. rw lem1. uf a; rw U_rw; lu. rw lem1. lu. rw lem1. uh H; ee. ap H6. uhg; ir. wr lem1. ap H3; am. rw lem1. uh H; ee. ap H9. wr lem1; am. wr lem1; am. Save. Lemma full_open : forall a, axioms a -> is_open a (U a). Proof. ir. uh H; ee. am. Qed. Lemma emptyset_open : forall a, axioms a -> is_open a emptyset. Proof. ir; uh H; ee; am. Qed. Lemma union_open : forall a z, axioms a -> (forall u, inc u z -> is_open a u) -> is_open a (union z). Proof. ir. uh H; ee. ap H3; am. Qed. Lemma intersection2_open : forall a u v, axioms a -> is_open a u -> is_open a v -> is_open a (intersection2 u v). Proof. ir. uh H; ee. ap H5; am. Qed. (*** defining a space using neighborhoods ***) Definition opens_dbn x (n:EP) := Z (powerset x) (fun u=> (forall p, inc p u -> exists v, (inc p v & sub v u & n v))). Lemma opens_dbn_inc_rw : forall x n u, inc u (opens_dbn x n) = (sub u x & (forall p, inc p u -> exists v, (inc p v & sub v u & n v))). Proof. ir. ap iff_eq; ir. ufi opens_dbn H; Ztac. wr powerset_inc_rw; am. ee. uf opens_dbn; ap Z_inc. rw powerset_inc_rw; am. am. Qed. Definition neighborhood_property x (n:EP) := (forall u, n u -> sub u x) & (forall p, inc p x -> exists u, (inc p u & n u)) & (forall p u v, inc p (intersection2 u v) -> n u -> n v -> (exists w, (inc p w & sub w (intersection2 u v) & n w))). Lemma dbn_properties : forall x n, neighborhood_property x n -> property x (opens_dbn x n). Proof. ir. uh H; ee. uhg; dj. uhg; ir. ufi opens_dbn H2; Ztac. rw opens_dbn_inc_rw. ee. ap sub_refl. ir. nin (H0 _ H3). sh x0; xd. rw opens_dbn_inc_rw. ee. uhg; ir. elim (B H4). ir. elim (B H4). rw opens_dbn_inc_rw. ee. uhg; ir. nin (union_exists H6). ee. uh H5. cp (H5 _ H8). rwi opens_dbn_inc_rw H9. ee. ap H9. am. ir. nin (union_exists H6). ee. uh H5. cp (H5 _ H8). rwi opens_dbn_inc_rw H9. ee. cp (H10 _ H7). nin H11. ee. sh x1; xd. uhg; ir; apply union_inc with x0. ap H12; am. am. rw opens_dbn_inc_rw. ee. rwi opens_dbn_inc_rw H6. rwi opens_dbn_inc_rw H7. ee. uhg; ir. ap H6. apply intersection2_first with v; am. ir. rwi opens_dbn_inc_rw H7. rwi opens_dbn_inc_rw H6. ee. cp (intersection2_first H8). cp (intersection2_second H8). cp (H10 _ H11). cp (H9 _ H12). nin H13. nin H14. ee. assert (inc p (intersection2 x0 x1)). ap intersection2_inc; am. cp (H1 _ _ _ H19 H18 H16). nin H20. sh x2; xd. uhg; ir. ap intersection2_inc. ap H17. apply intersection2_first with x1. ap H21; am. ap H15. apply intersection2_second with x0. ap H21; am. Qed. Definition dbn x n := create_ens x (opens_dbn x n) (da Structure) (da Distance). Lemma dbn_axioms : forall x n, neighborhood_property x n -> axioms (dbn x n). Proof. ir. uf dbn. ap create_axioms. ap dbn_properties. am. Qed. Lemma dbn_U_rw : forall x n, (U (dbn x n)) = x. Proof. ir. uf dbn. rw U_rw; tv. Qed. Lemma dbn_open_rw : forall x n u, neighborhood_property x n -> is_open (dbn x n) u = (sub u x & (forall p, inc p u -> exists v, (inc p v & sub v u & n v))). Proof. ir. ap iff_eq; ir. ufi dbn H0. uh H0. nin H0. rwi opens_rw H1. rwi opens_dbn_inc_rw H1. am. ee. uf dbn. uhg; ee. rw U_rw. am. rw opens_rw. rw opens_dbn_inc_rw. ee; try am. Qed. Lemma dbn_neighborhood_open : forall x n u, neighborhood_property x n -> n u -> is_open (dbn x n) u. Proof. ir. rw dbn_open_rw. ee. uh H; ee. ap H; am. ir. sh u. ee; try am. ap sub_refl. am. Qed. Definition cartesian2_nbd a b y := axioms a & axioms b & (exists u, exists v, is_open a u & is_open b v & y = Cartesian.product u v). Notation cartesian2 := Cartesian.product. Lemma cartesian2_domain : forall x y, nonempty y -> domain (cartesian2 x y) = x. Proof. ir. uf domain. ap extensionality; uhg; ir. rwi Image.inc_rw H0. nin H0; ee. cp (Cartesian.product_pr H0). ee. wr H1; am. rw Image.inc_rw. nin H. sh (pair x0 y0). rw pr1_pair; ee; try tv. ap Cartesian.product_pair_inc; am. Qed. Lemma cartesian2_domain_or : forall x y, domain (cartesian2 x y) = x \/ domain (cartesian2 x y) = emptyset. Proof. ir. apply by_cases with (nonempty y); ir. ap or_introl. ap cartesian2_domain; am. ap or_intror. ap extensionality; uhg; ir. ufi domain H0; rwi Image.inc_rw H0. nin H0. ee. cp (Cartesian.product_pr H0). ee. assert False. ap H. sh (pr2 x1). am. elim H5. elim (B H0). Qed. Lemma cartesian2_range: forall x y, nonempty x -> range (cartesian2 x y) = y. Proof. ir. uf range. ap extensionality; uhg; ir. rwi Image.inc_rw H0. nin H0; ee. cp (Cartesian.product_pr H0). ee. wr H1; am. rw Image.inc_rw. nin H. sh (pair y0 x0). rw pr2_pair; ee; try tv. ap Cartesian.product_pair_inc; am. Qed. Lemma cartesian2_range_or : forall x y, range (cartesian2 x y) = y \/ range (cartesian2 x y) = emptyset. Proof. ir. apply by_cases with (nonempty x); ir. ap or_introl. ap cartesian2_range; am. ap or_intror. ap extensionality; uhg; ir. ufi range H0; rwi Image.inc_rw H0. nin H0. ee. cp (Cartesian.product_pr H0). ee. assert False. ap H. sh (pr1 x1). am. elim H5. elim (B H0). Qed. Lemma domain_emptyset : domain emptyset = emptyset. Proof. uf domain; ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. elim (B H). elim (B H). Qed. Lemma range_emptyset : range emptyset = emptyset. Proof. uf range; ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. elim (B H). elim (B H). Qed. Lemma if_domain_empty : forall y, domain y = emptyset -> y = emptyset. Proof. ir. ap extensionality; uhg; ir. assert (inc (pr1 x) (domain y)). uf domain; rw Image.inc_rw. sh x; xd. rwi H H1. elim (B H1). elim (B H0). Qed. Lemma if_range_empty : forall y, range y = emptyset -> y = emptyset. Proof. ir. ap extensionality; uhg; ir. assert (inc (pr2 x) (range y)). uf range; rw Image.inc_rw. sh x; xd. rwi H H1. elim (B H1). elim (B H0). Qed. Lemma cartesian2_emptyset_left : forall y, cartesian2 emptyset y = emptyset. Proof. ir. cp (cartesian2_domain_or emptyset y). nin H. cp (if_domain_empty H). am. cp (if_domain_empty H). am. Qed. Lemma cartesian2_emptyset_right : forall x, cartesian2 x emptyset = emptyset. Proof. ir. cp (cartesian2_range_or x emptyset). nin H. cp (if_range_empty H). am. cp (if_range_empty H). am. Qed. Lemma cartesian2_nbd_rw : forall a b y, axioms a -> axioms b -> cartesian2_nbd a b y = (is_open a (domain y) & is_open b (range y) & y = cartesian2 (domain y) (range y)). Proof. ir. ap iff_eq; ir. uh H1. nin H1. nin H2. nin H3. nin H3. nin (cartesian2_domain_or x x0). nin (cartesian2_range_or x x0). assert (lem1: domain y = x). ee. rw H7; am. assert (lem2: range y = x0). ee. rw H7; am. rw lem1. rw lem2. am. assert (range y = emptyset). ee. rw H7; am. cp (if_range_empty H6). rw H7. rw domain_emptyset. rw range_emptyset. ee. lu. lu. rw cartesian2_emptyset_left. tv. cp (if_domain_empty H4). nin H3. nin H6. wri H7 H5. rw H5. rw domain_emptyset. rw range_emptyset. ee. lu. lu. rw cartesian2_emptyset_left. tv. uhg. xd. sh (domain y). sh (range y). xd. Qed. Lemma cartesian_product_intersect : forall x y z w, intersection2 (cartesian2 x y) (cartesian2 z w) = cartesian2 (intersection2 x z) (intersection2 y w). Proof. ir. ap extensionality; uhg; ir. cp (intersection2_first H); cp (intersection2_second H). cp (product_pr H0); cp (product_pr H1); ee. ap product_inc; try am; ap intersection2_inc; am. cp (product_pr H). ee. cp (intersection2_first H1); cp (intersection2_second H1). cp (intersection2_first H2); cp (intersection2_second H2). ap intersection2_inc; ap product_inc; am. Qed. Definition cartesian2_top a b := dbn (cartesian2 (U a) (U b)) (cartesian2_nbd a b). Lemma cartesian2_top_U_rw : forall a b, U (cartesian2_top a b) = cartesian2 (U a) (U b). Proof. ir. uf cartesian2_top. rw dbn_U_rw. tv. Qed. Lemma cartesian2_sub : forall x y u v, sub x u -> sub y v -> sub (cartesian2 x y) (cartesian2 u v). Proof. ir. uhg; ir. cp (product_pr H1); ee. ap product_inc. am. ap H; am. ap H0; am. Qed. Lemma cartesian2_nbd_property : forall a b, axioms a -> axioms b -> neighborhood_property (product (U a) (U b)) (cartesian2_nbd a b). Proof. ir. uhg; dj. rwi cartesian2_nbd_rw H1. ee. rw H3; ap cartesian2_sub. lu. lu. am. am. sh (cartesian2 (U a) (U b)). ee; try am. uhg; ee. am. am. sh (U a). sh (U b). ee. lu. lu. tv. rwi cartesian2_nbd_rw H4; rwi cartesian2_nbd_rw H5; ee. sh (cartesian2 (intersection2 (domain u) (domain v)) (intersection2 (range u) (range v))). ee. wr cartesian_product_intersect. wr H9. wr H7. am. uhg; ir. wri cartesian_product_intersect H10. wri H9 H10. wri H7 H10. am. uhg; ee. am. am. sh (intersection2 (domain u) (domain v)). sh (intersection2 (range u) (range v)). ee. ap intersection2_open. am. am. am. ap intersection2_open; am. tv. am. am. am. am. am. am. am. am. Qed. Lemma cartesian2_top_axioms : forall a b, axioms a -> axioms b -> axioms (cartesian2_top a b). Proof. ir. uf cartesian2_top. ap dbn_axioms. ap cartesian2_nbd_property. am. am. Qed. Lemma open_by_nbd : forall a u, axioms a -> (forall p, inc p u -> (exists v, inc p v & sub v u & is_open a v)) -> is_open a u. Proof. ir. pose (z:= Z (opens a) (fun v => sub v u)). assert (u = union z). ap extensionality; uhg; ir. cp (H0 _ H1). nin H2. ee. apply union_inc with x0. am. uf z; ap Z_inc. lu. am. cp (union_exists H1). nin H2. ee. ufi z H3; Ztac. rw H1. ap union_open. am. ir. ufi z H2; Ztac. uhg; ee; try am. uh H; ee. cp (H _ H3). rwi powerset_inc_rw H9. am. Qed. Lemma cartesian2_open_vertical_slice : forall a b x u, axioms a -> axioms b -> inc x (U a) -> is_open (cartesian2_top a b) u -> is_open b (Z (U b) (fun y=> (inc (pair x y) u))). Proof. ir. ap open_by_nbd. am. ir. Ztac. ufi cartesian2_top H2. rwi dbn_open_rw H2. ee. cp (H6 _ H5). nin H7. ee. sh (range x0). ee. uf range; rw Image.inc_rw. sh (pair x p). ee; try am. rw pr2_pair; tv. uhg; ir. ap Z_inc. ufi range H10. rwi Image.inc_rw H10. nin H10. ee. assert (U b= range (product (U a) (U b))). rw cartesian2_range. tv. sh x; am. rw H12. uf range; rw Image.inc_rw. sh x2. ee. ap H2. ap H8; am. am. rwi cartesian2_nbd_rw H9. ee. ap H8. rw H12. ap product_pair_inc. uf domain; rw Image.inc_rw. sh (pair x p). ee; try am. rw pr1_pair; tv. am. am. am. rwi cartesian2_nbd_rw H9; ee; am. ap cartesian2_nbd_property; am. Qed. Lemma cartesian2_open_horizontal_slice : forall a b y u, axioms a -> axioms b -> inc y (U b) -> is_open (cartesian2_top a b) u -> is_open a (Z (U a) (fun x=> (inc (pair x y) u))). Proof. ir. ap open_by_nbd. am. ir. Ztac. ufi cartesian2_top H2. rwi dbn_open_rw H2. ee. cp (H6 _ H5). nin H7. ee. sh (domain x). ee. uf domain; rw Image.inc_rw. sh (pair p y). ee; try am. rw pr1_pair; tv. uhg; ir. ap Z_inc. ufi domain H10. rwi Image.inc_rw H10. nin H10. ee. assert (U a= domain (product (U a) (U b))). rw cartesian2_domain. tv. sh y; am. rw H12. uf domain; rw Image.inc_rw. sh x1. ee. ap H2. ap H8; am. am. rwi cartesian2_nbd_rw H9. ee. ap H8. rw H12. ap product_pair_inc. am. uf range; rw Image.inc_rw. sh (pair p y). ee; try am. rw pr2_pair; tv. am. am. rwi cartesian2_nbd_rw H9; ee; am. ap cartesian2_nbd_property; am. Qed. Definition is_disconnected a := axioms a & exists u, is_open a u & nonempty u & is_open a (complement (U a) u) & nonempty (complement (U a) u). Definition is_connected a := axioms a & ~(is_disconnected a). Lemma cartesian2_nonempty : forall x y, nonempty x -> nonempty y -> nonempty (cartesian2 x y). Proof. ir. nin H; nin H0. sh (pair y0 y1). ap product_inc. ap pair_is_pair. rw pr1_pair; am. rw pr2_pair; am. Qed. Lemma emptyset_connected : forall a, axioms a -> (U a) = emptyset -> is_connected a. Proof. ir. uhg; ee; try am; uhg; ir. uh H1; ee. nin H2; ee. nin H3. uh H2; ee. cp (H2 _ H3). rwi H0 H7; elim (B H7). Qed. Lemma complement_or : forall x y z, inc x y -> (inc x z \/ inc x (complement y z)). Proof. ir. apply by_cases with (inc x z). ir. ap or_introl; am. ir. ap or_intror. rw inc_complement. xd. Qed. Lemma cartesian2_connected : forall a b, is_connected a -> is_connected b -> is_connected (cartesian2_top a b). Proof. ir. uhg; ee. ap cartesian2_top_axioms. lu. lu. uhg; ir. uh H1; ee. nin H2; ee. (*** on a maintenant l'ouvert x qui est nonvide H3 ***) nin H3. pose (u:= pr1 y). pose (v:= pr2 y). assert (y = pair u v). uh H2; ee. cp (H2 _ H3). ufi cartesian2_top H7. rwi dbn_U_rw H7. cp (product_pr H7); ee. cp (pair_recov H8). uh H11. sy; am. (*** on utilise que le complementaire est nonvide ***) pose (z:= complement (U (cartesian2_top a b)) x). cp H5. fold z in H7. nin H7. pose (u0:= pr1 y0). pose (v0:= pr2 y0). assert (y0 = pair u0 v0). fold z in H4; uh H4; ee. cp (H4 _ H7). ufi cartesian2_top H9. rwi dbn_U_rw H9. cp (product_pr H9); ee. cp (pair_recov H10). uh H13. sy; am. (*** on remarque que u et u0 sont dans (U a) et v et v0 sont dans (U b) *****) assert (lem1 : inc y (cartesian2 (U a) (U b))). uh H2; ee. rwi cartesian2_top_U_rw H2. ap H2; am. assert (lem2 : inc y0 (cartesian2 (U a) (U b))). uh H4; ee. rwi cartesian2_top_U_rw H4. ap H4. wr cartesian2_top_U_rw. am. assert (lem3 : inc u (U a)). uf u. cp (product_pr lem1); xd. assert (lem4 : inc u0 (U a)). uf u0. cp (product_pr lem2); xd. assert (lem5 : inc v (U b)). uf v. cp (product_pr lem1); xd. assert (lem6 : inc v0 (U b)). uf v0. cp (product_pr lem2); xd. (*** maintenant on a (pair u v) dans x et (pair u0 v0) dans le complementaire. On raison par cas, soit (pair u v0) dans x, soit dans le complementaire ***) assert (lem7 : inc (pair u v0) (U (cartesian2_top a b))). uf cartesian2_top; rw dbn_U_rw. ap product_pair_inc; am. cp (complement_or x lem7). nin H9. (*** maintenant on est dans le cas inc (pair u v0) x dans ce cas on regarde la tranche horizontal en v0 ***) pose (e := Z (U a) (fun t => inc (pair t v0) x)). assert (lem8 : complement (U a) e = Z (U a) (fun t => inc (pair t v0) z)). ap extensionality; uhg; ir. rwi inc_complement H10. ee. ap Z_inc. am. uf z. rw inc_complement. ee. rw cartesian2_top_U_rw. ap product_pair_inc; am. uhg; ir. ap H11. uf e; ap Z_inc. am. am. Ztac. rw inc_complement. ee; try am. uhg; ir. ufi e H13. Ztac. ufi z H12. rwi inc_complement H12. ee. ap H16. am. (*** fin de la demo de lem8 *******) (*** maintenant on peut montrer la disconnexite de a utilisant e ***) uh H. ee. ap H10. (*** c'etait ce qui disait que a n'est pas disconnexe ****) uhg. ee; try am. sh e. ee. (*** prouver que e est open ***) uf e. apply cartesian2_open_horizontal_slice with b. am. lu. am. am. (*** pour montrer que e est nonvide on montre l'element u ***) sh u. uf e. ap Z_inc. am. am. (*** prouver que le complementaire de e est ouvert c'etait la raison pour lem8 *****) rw lem8. apply cartesian2_open_horizontal_slice with b. am. lu. am. am. (*** pour montrer que le complementaire de e est nonvide on montre l'element u0 *******) sh u0. rw lem8. ap Z_inc. am. wr H8; am. (**** ca y est pour ce cas ******) (**** maintenant on traite l'autre cas de la meme facon mais en regardant la tranche verticale en u on peut noter que la meme demo s'applique beaucoup *******************************************) pose (e := Z (U b) (fun t => inc (pair u t) x)). assert (lem9 : complement (U b) e = Z (U b) (fun t => inc (pair u t) z)). ap extensionality; uhg; ir. rwi inc_complement H10. ee. ap Z_inc. am. uf z. rw inc_complement. ee. rw cartesian2_top_U_rw. ap product_pair_inc; am. uhg; ir. ap H11. uf e; ap Z_inc. am. am. Ztac. rw inc_complement. ee; try am. uhg; ir. ufi e H13. Ztac. ufi z H12. rwi inc_complement H12. ee. ap H16. am. (*** fin de la demo de lem8 *******) (*** maintenant on peut montrer la disconnexite de b cette fois, utilisant e ***) uh H0. ee. ap H10. (*** c'etait ce qui disait que a n'est pas disconnexe ****) uhg. ee; try am. sh e. ee. (*** prouver que e est open ***) uf e. apply cartesian2_open_vertical_slice with a. lu. am. am. am. (*** pour montrer que e est nonvide on montre l'element v ***) sh v. uf e. ap Z_inc. am. wr H6; am. (*** prouver que le complementaire de e est ouvert c'etait la raison pour lem9 *****) rw lem9. apply cartesian2_open_vertical_slice with a. lu. am. am. am. (*** pour montrer que le complementaire de e est nonvide on montre l'element v0 *******) sh v0. rw lem9. ap Z_inc. am. uf z. am. Qed. End Topology.