From 2d9acc81b9a445251e12e048288b8691f3d40172 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 5 Oct 2022 20:12:57 -0400 Subject: [PATCH 1/9] swapping machines --- theories/topology.v | 82 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/theories/topology.v b/theories/topology.v index 020038f8f3..43b85f98cc 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3485,6 +3485,86 @@ End DiscreteTopology. #[global] Hint Resolve discrete_bool : core. +Definition separates_points_from_closed {I : Type} {T : topologicalType} + {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := + forall (U : set T) x, + closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). + +Section product_embeddings. +Context {I : choiceType} {R : realType} {T : topologicalType}. +Context {U_ : I -> topologicalType}. +Variable (f_ : forall i, (T -> U_ i)). + +Hypothesis sepf : separates_points_from_closed f_. +Hypothesis ctsf : forall i, continuous (f_ i). + +Let weakT := @sup_topologicalType T I (fun i => Topological.class + (weak_topologicalType (f_ i))). +Let PU := product_topologicalType U_. + +Lemma weak_sep_cvg (F : set (set T)) (x : T) : + Filter F -> + (F --> (x : T)) <-> (F --> (x : weakT)). +Proof. +move=> FF; split. + move=> FTx; apply/cvg_sup => i U /=. + have -> := @nbhsE (weak_topologicalType (f_ i)) x. + case=> B [[[C oC <- Cfx]]] /filterS; apply; apply: FTx => /=. + by rewrite nbhsE; exists (f_ i @^-1` C); repeat split => //; exact: open_comp. +move/cvg_sup => wiFx U /=; rewrite nbhs_simpl nbhsE => [[B [[oB Bx]]]]. +move/filterS; apply; have nBx : ~ (~`B) x by []. +have [i nclfix] := sepf (open_closedC oB) nBx. +apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. +exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //. + apply: open_comp; last by rewrite ?openC; last apply: closed_closure. + by move=> + _; exact: weak_continuous. +rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. +by move/forall2NP => /(_ z) [] //= /contrapT. +Qed. + +Lemma weak_sep_nbhsE x : + @nbhs T T x = @nbhs T weakT x. +Proof. +rewrite predeqE => U; split; move: U. + have P := @weak_sep_cvg (@nbhs T weakT x) x (nbhs_filter (x : weakT)). + exact/P. +have P := @weak_sep_cvg (@nbhs T T x) x (nbhs_filter (x : T)). +exact/P. +Qed. + +Definition join_product (x : weakT) : PU := fun i => f_ i x. + +Lemma join_product_continuous : continuous join_product. +Proof. +move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). +move=> i; move: x. +apply/(@continuousP _ (weak_topologicalType _)) => A [B oB <-]. +rewrite (_ : @^~ i = prod_topo_apply i) //. +suff : forall C, join_product @^-1` (prod_topo_apply i @^-1` C) = f_ i @^-1` C. + move/(_ B) => ->; apply: open_comp => // + _; rewrite /cvg_to /= => x U //=. + rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. + apply: weak_continuous. +rewrite [join_product @^-1` _](_ : join_product _ = f_ i @^-1` _). + + + + +Lemma weak_sep_cvg (F : set (set T)) (x : T) : + Filter F -> + (F --> (x : T)) = (F --> (x : weakT)). +Proof. + + rewrite (@nbhs (x : weak_topologicalType (f_ i))). + Search nbhs open_nbhs. + Search (cvg_to) open. + + rewrite /open /=. + +End product_embeddings. + + + + (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -6632,6 +6712,8 @@ move/nbhs_singleton: nbhsU; move: x; apply/in_setP. by rewrite -continuous_open_subspace. Unshelve. end_near. Qed. +Definition separates_points_from_sets {} + Section UniformPointwise. Context {U : topologicalType} {V : uniformType}. From f114567cbad6e73c8a31b65e4f0c23629756ad71 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 6 Oct 2022 00:45:08 -0400 Subject: [PATCH 2/9] proof of open map --- theories/topology.v | 162 ++++++++++++++++++++++++-------------------- 1 file changed, 87 insertions(+), 75 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 43b85f98cc..0802b9cd9c 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3490,79 +3490,6 @@ Definition separates_points_from_closed {I : Type} {T : topologicalType} forall (U : set T) x, closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). -Section product_embeddings. -Context {I : choiceType} {R : realType} {T : topologicalType}. -Context {U_ : I -> topologicalType}. -Variable (f_ : forall i, (T -> U_ i)). - -Hypothesis sepf : separates_points_from_closed f_. -Hypothesis ctsf : forall i, continuous (f_ i). - -Let weakT := @sup_topologicalType T I (fun i => Topological.class - (weak_topologicalType (f_ i))). -Let PU := product_topologicalType U_. - -Lemma weak_sep_cvg (F : set (set T)) (x : T) : - Filter F -> - (F --> (x : T)) <-> (F --> (x : weakT)). -Proof. -move=> FF; split. - move=> FTx; apply/cvg_sup => i U /=. - have -> := @nbhsE (weak_topologicalType (f_ i)) x. - case=> B [[[C oC <- Cfx]]] /filterS; apply; apply: FTx => /=. - by rewrite nbhsE; exists (f_ i @^-1` C); repeat split => //; exact: open_comp. -move/cvg_sup => wiFx U /=; rewrite nbhs_simpl nbhsE => [[B [[oB Bx]]]]. -move/filterS; apply; have nBx : ~ (~`B) x by []. -have [i nclfix] := sepf (open_closedC oB) nBx. -apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. -exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //. - apply: open_comp; last by rewrite ?openC; last apply: closed_closure. - by move=> + _; exact: weak_continuous. -rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. -by move/forall2NP => /(_ z) [] //= /contrapT. -Qed. - -Lemma weak_sep_nbhsE x : - @nbhs T T x = @nbhs T weakT x. -Proof. -rewrite predeqE => U; split; move: U. - have P := @weak_sep_cvg (@nbhs T weakT x) x (nbhs_filter (x : weakT)). - exact/P. -have P := @weak_sep_cvg (@nbhs T T x) x (nbhs_filter (x : T)). -exact/P. -Qed. - -Definition join_product (x : weakT) : PU := fun i => f_ i x. - -Lemma join_product_continuous : continuous join_product. -Proof. -move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). -move=> i; move: x. -apply/(@continuousP _ (weak_topologicalType _)) => A [B oB <-]. -rewrite (_ : @^~ i = prod_topo_apply i) //. -suff : forall C, join_product @^-1` (prod_topo_apply i @^-1` C) = f_ i @^-1` C. - move/(_ B) => ->; apply: open_comp => // + _; rewrite /cvg_to /= => x U //=. - rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. - apply: weak_continuous. -rewrite [join_product @^-1` _](_ : join_product _ = f_ i @^-1` _). - - - - -Lemma weak_sep_cvg (F : set (set T)) (x : T) : - Filter F -> - (F --> (x : T)) = (F --> (x : weakT)). -Proof. - - rewrite (@nbhs (x : weak_topologicalType (f_ i))). - Search nbhs open_nbhs. - Search (cvg_to) open. - - rewrite /open /=. - -End product_embeddings. - - (** * Uniform spaces *) @@ -6608,6 +6535,93 @@ Qed. End SubspaceWeak. +Section product_embeddings. +Context {I : choiceType} {T : topologicalType}. +Context {U_ : I -> topologicalType}. +Variable (f_ : forall i, (T -> U_ i)). + +Hypothesis sepf : separates_points_from_closed f_. +Hypothesis ctsf : forall i, continuous (f_ i). + +Let weakT := @sup_topologicalType T I (fun i => Topological.class + (weak_topologicalType (f_ i))). +Let PU := product_topologicalType U_. + +Lemma weak_sep_cvg (F : set (set T)) (x : T) : + Filter F -> + (F --> (x : T)) <-> (F --> (x : weakT)). +Proof. +move=> FF; split. + move=> FTx; apply/cvg_sup => i U /=. + have -> := @nbhsE (weak_topologicalType (f_ i)) x. + case=> B [[[C oC <- Cfx]]] /filterS; apply; apply: FTx => /=. + by rewrite nbhsE; exists (f_ i @^-1` C); repeat split => //; exact: open_comp. +move/cvg_sup => wiFx U /=; rewrite nbhs_simpl nbhsE => [[B [[oB Bx]]]]. +move/filterS; apply; have nBx : ~ (~`B) x by []. +have [i nclfix] := sepf (open_closedC oB) nBx. +apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. +exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //. + apply: open_comp; last by rewrite ?openC; last apply: closed_closure. + by move=> + _; exact: weak_continuous. +rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. +by move/forall2NP => /(_ z) [] //= /contrapT. +Qed. + +Lemma weak_sep_nbhsE x : + @nbhs T T x = @nbhs T weakT x. +Proof. +rewrite predeqE => U; split; move: U. + have P := @weak_sep_cvg (@nbhs T weakT x) x (nbhs_filter (x : weakT)). + exact/P. +have P := @weak_sep_cvg (@nbhs T T x) x (nbhs_filter (x : T)). +exact/P. +Qed. + +Lemma weak_sep_openE : + @open T = @open weakT. +Proof. +rewrite predeqE => A; split; rewrite ? openE => P z => /P. + by rewrite /= /interior weak_sep_nbhsE. +by rewrite /= /interior weak_sep_nbhsE. +Qed. + +Definition join_product (x : weakT) : PU := fun i => f_ i x. + +Lemma join_product_continuous : continuous join_product. +Proof. +move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). +move=> i; move: x. +apply/(@continuousP _ (weak_topologicalType _)) => A [B oB <-]. +rewrite (_ : @^~ i = prod_topo_apply i) //. +have -> : join_product @^-1` (prod_topo_apply i @^-1` B) = f_ i @^-1` B by []. +apply: open_comp => // + _; rewrite /cvg_to => x U //=. +rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. +Qed. + +Lemma join_product_open : forall (A : set weakT), open A -> + open ((join_product @` A) : set (subspace (join_product @` setT))). +Proof. +move=> A; rewrite -weak_sep_openE => oA. +have S := @sepf (~` A) _ (open_closedC oA). +rewrite openE => y /= [x Ax] jxy; rewrite /interior. +have [// | i nAfiy] := S x. +pose B := prod_topo_apply i @^-1` (~` closure (f_ i @` ~` A)). +apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). + move=> z [[w ?]] wzE Bz; exists w => //. + move: Bz; rewrite /B -wzE /preimage /mkset closureC. + case=> K /= [oK KsubA] => /KsubA /=. + have -> : prod_topo_apply i (join_product w) = f_ i w by []. + by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. +apply: open_nbhs_nbhs; split; last by rewrite -jxy. +apply: openI. + apply: open_subspaceT. +apply: open_subspaceW. + apply: open_comp; first by move=> + _; apply: prod_topo_apply_continuous. + by apply: closed_openC; exact: closed_closure. +Qed. + +End product_embeddings. + Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : {within A, continuous f} -> compact A -> compact (f @` A). Proof. @@ -6712,8 +6726,6 @@ move/nbhs_singleton: nbhsU; move: x; apply/in_setP. by rewrite -continuous_open_subspace. Unshelve. end_near. Qed. -Definition separates_points_from_sets {} - Section UniformPointwise. Context {U : topologicalType} {V : uniformType}. From 5591c9814f5f0b0837ed7cd7402925e0c9ffe811 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 6 Oct 2022 11:10:08 -0400 Subject: [PATCH 3/9] hausdorff accessible --- theories/topology.v | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/theories/topology.v b/theories/topology.v index 0802b9cd9c..deb8a78a47 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3131,7 +3131,6 @@ Proof. move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //. by rewrite nbhsE inE; exists A; do !split=> //; rewrite inE in xA. Qed. - Definition close x y : Prop := forall M, open_nbhs y M -> closure M x. Lemma closeEnbhs x : close x = cluster (nbhs x). @@ -3204,6 +3203,13 @@ move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)). by rewrite -set0P => /(_ _ _)/negP; apply. Qed. +Definition hausdorff_accessible : hausdorff_space T -> accessible_space. +Proof. +rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP]. +rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. +by rewrite inE; apply: VUc; rewrite -inE. +Qed. + Hypothesis sep : hausdorff_space T. Lemma closeE x y : close x y = (x = y). @@ -6620,6 +6626,20 @@ apply: open_subspaceW. by apply: closed_openC; exact: closed_closure. Qed. +Lemma join_product_inj : accessible_space T -> + set_inj [set: T] join_product. +Proof. +move=> /accessible_closed_set1 cl1 x y. +case: (eqVneq x y) => // xny _ _ jxjy. +have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP. +move=> i clfxy; suff : join_product x i != join_product y i. + by rewrite jxjy => /eqP. +apply/negP; move: clfxy; apply: contra_not => /eqP; rewrite /join_product => ->. +by apply subset_closure; exists y. +Qed. + +Search hausdorff_space accessible_space. + End product_embeddings. Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : From 5a9187bdf3655827db6488ac82b3e50d357eab0f Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 6 Oct 2022 13:46:11 -0400 Subject: [PATCH 4/9] weak products equivalent --- theories/topology.v | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index deb8a78a47..d14241a4a4 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6619,26 +6619,35 @@ apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). have -> : prod_topo_apply i (join_product w) = f_ i w by []. by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. apply: open_nbhs_nbhs; split; last by rewrite -jxy. -apply: openI. - apply: open_subspaceT. -apply: open_subspaceW. - apply: open_comp; first by move=> + _; apply: prod_topo_apply_continuous. - by apply: closed_openC; exact: closed_closure. +apply: openI; first exact: open_subspaceT. +apply: open_subspaceW; apply: open_comp. + by move=> + _; exact: prod_topo_apply_continuous. +by apply: closed_openC; exact: closed_closure. Qed. -Lemma join_product_inj : accessible_space T -> - set_inj [set: T] join_product. +Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A]. +Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed. + +Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product. Proof. -move=> /accessible_closed_set1 cl1 x y. -case: (eqVneq x y) => // xny _ _ jxjy. +move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy. have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP. -move=> i clfxy; suff : join_product x i != join_product y i. - by rewrite jxjy => /eqP. -apply/negP; move: clfxy; apply: contra_not => /eqP; rewrite /join_product => ->. +move=> i P; suff : join_product x i != join_product y i by rewrite jxjy => /eqP. +apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. by apply subset_closure; exists y. Qed. -Search hausdorff_space accessible_space. +Lemma join_product_weak : accessible_space T -> + @open weakT = @open (weak_topologicalType join_product). +Proof. +move=> /join_product_inj => inj; rewrite predeqE => U; split; first last. + by move=> [V ? <-]; apply open_comp => // + _; exact: join_product_continuous. +move=> /join_product_open/open_subspaceP [V [oU VU]]. +exists V => //; have := @f_equal _ _ (preimage join_product) _ _ VU. +rewrite !preimage_setI // !preimage_range !setIT => ->. +rewrite eqEsubset; split; last exact: preimage_image. +by move=> z [w Uw] /inj <- //; rewrite inE. +Qed. End product_embeddings. From 5bc1e3a69ca2f6d9e90e796c317b06b2130075d2 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 6 Oct 2022 14:13:08 -0400 Subject: [PATCH 5/9] changelog --- CHANGELOG_UNRELEASED.md | 7 +++++++ classical/classical_sets.v | 3 +++ theories/topology.v | 28 ++++++++++++++-------------- 3 files changed, 24 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4733f343d0..0352eb101a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -98,6 +98,13 @@ + lemma `fsumEFin` - in `lebesgue_measure.v`: + definition `ErealGenInftyO.R` and lemma `ErealGenInftyO.measurableE` +- in `classical_sets.v`: + + lemma `preimage_range` +- in `topology.v` + + definition `separates_points_from_closed`, `join_product` + + lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, + `join_product_continuous`, `join_product_open`, `join_product_inj`, + `join_product_weak` ### Changed - in `topology.v` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index e9c0138345..513b242649 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1226,6 +1226,9 @@ Proof. by case=> [t ?]; exists (f t). Qed. Lemma preimage_image f A : A `<=` f @^-1` (f @` A). Proof. by move=> a Aa; exists a. Qed. +Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A]. +Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed. + Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y. Proof. by move=> _ [t /= Yft <-]. Qed. diff --git a/theories/topology.v b/theories/topology.v index d14241a4a4..945214e0d5 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3491,13 +3491,6 @@ End DiscreteTopology. #[global] Hint Resolve discrete_bool : core. -Definition separates_points_from_closed {I : Type} {T : topologicalType} - {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := - forall (U : set T) x, - closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). - - - (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -6541,6 +6534,18 @@ Qed. End SubspaceWeak. +Definition separates_points_from_closed {I : Type} {T : topologicalType} + {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := + forall (U : set T) x, + closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). + +(* A handy technique for emebdding a space T into a product. The key interface + is 'separates_points_from_closed', which guarantees that the topologies + - T's native topology + - sup (weak f_i) - the sup of all the weak topologies of f_i + - weak (x => (f_1 x, f_2 x,...)) - the weak topology from the product space + are equivalent (the last equivalence seems to require accessible_space). +*) Section product_embeddings. Context {I : choiceType} {T : topologicalType}. Context {U_ : I -> topologicalType}. @@ -6577,10 +6582,8 @@ Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x. Proof. rewrite predeqE => U; split; move: U. - have P := @weak_sep_cvg (@nbhs T weakT x) x (nbhs_filter (x : weakT)). - exact/P. -have P := @weak_sep_cvg (@nbhs T T x) x (nbhs_filter (x : T)). -exact/P. + by have P := weak_sep_cvg x (nbhs_filter (x : weakT)); exact/P. +by have P := weak_sep_cvg x (nbhs_filter (x : T)); exact/P. Qed. Lemma weak_sep_openE : @@ -6625,9 +6628,6 @@ apply: open_subspaceW; apply: open_comp. by apply: closed_openC; exact: closed_closure. Qed. -Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A]. -Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed. - Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product. Proof. move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy. From 98478a4df902427d6936b85643576d223c5ec878 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 6 Oct 2022 15:10:13 -0400 Subject: [PATCH 6/9] strengthen join_product_weak --- CHANGELOG_UNRELEASED.md | 1 + theories/topology.v | 82 ++++++++++++++++++++--------------------- 2 files changed, 42 insertions(+), 41 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0352eb101a..a30a36ab2e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -102,6 +102,7 @@ + lemma `preimage_range` - in `topology.v` + definition `separates_points_from_closed`, `join_product` + + lemma `hausdorff_accessible` + lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, `join_product_continuous`, `join_product_open`, `join_product_inj`, `join_product_weak` diff --git a/theories/topology.v b/theories/topology.v index 945214e0d5..17f04bc25c 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -116,6 +116,13 @@ Require Import mathcomp_extra reals signed. (* \oo == "eventually" filter on nat: set of *) (* predicates on natural numbers that are *) (* eventually true. *) +(* separates_points_from_closed f == For a closed set U and point x outside *) +(* some member of the family `f` sends *) +(* f_i(x) outside (closure (f_i@` U)). *) +(* used together with `join_product` *) +(* join_product f == The function (x i => f i x). When the *) +(* family f separates points from closed *) +(* sets, join_product is an embedding *) (* *) (* * Near notations and tactics: *) (* --> The purpose of the near notations and tactics is to make the *) @@ -6534,9 +6541,9 @@ Qed. End SubspaceWeak. -Definition separates_points_from_closed {I : Type} {T : topologicalType} - {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := - forall (U : set T) x, +Definition separates_points_from_closed {I : Type} {T : topologicalType} + {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := + forall (U : set T) x, closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). (* A handy technique for emebdding a space T into a product. The key interface @@ -6554,78 +6561,71 @@ Variable (f_ : forall i, (T -> U_ i)). Hypothesis sepf : separates_points_from_closed f_. Hypothesis ctsf : forall i, continuous (f_ i). -Let weakT := @sup_topologicalType T I (fun i => Topological.class - (weak_topologicalType (f_ i))). +Let weakT := @sup_topologicalType T I + (fun i => Topological.class (weak_topologicalType (f_ i))). Let PU := product_topologicalType U_. -Lemma weak_sep_cvg (F : set (set T)) (x : T) : - Filter F -> - (F --> (x : T)) <-> (F --> (x : weakT)). +Lemma weak_sep_cvg (F : set (set T)) (x : T) : + Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)). Proof. move=> FF; split. - move=> FTx; apply/cvg_sup => i U /=. - have -> := @nbhsE (weak_topologicalType (f_ i)) x. - case=> B [[[C oC <- Cfx]]] /filterS; apply; apply: FTx => /=. - by rewrite nbhsE; exists (f_ i @^-1` C); repeat split => //; exact: open_comp. -move/cvg_sup => wiFx U /=; rewrite nbhs_simpl nbhsE => [[B [[oB Bx]]]]. -move/filterS; apply; have nBx : ~ (~`B) x by []. -have [i nclfix] := sepf (open_closedC oB) nBx. + move=> FTx; apply/cvg_sup => i U. + have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. + case=> B [[[C oC <- ?]]] /filterS; apply; apply: FTx; rewrite /= nbhsE. + by exists (f_ i @^-1` C); repeat split => //; exact: open_comp. +move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [[oB ?]]]]. +move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //. apply: open_comp; last by rewrite ?openC; last apply: closed_closure. by move=> + _; exact: weak_continuous. rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. -by move/forall2NP => /(_ z) [] //= /contrapT. +by move/forall2NP => /(_ z) [] // /contrapT. Qed. -Lemma weak_sep_nbhsE x : - @nbhs T T x = @nbhs T weakT x. +Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x. Proof. rewrite predeqE => U; split; move: U. by have P := weak_sep_cvg x (nbhs_filter (x : weakT)); exact/P. by have P := weak_sep_cvg x (nbhs_filter (x : T)); exact/P. Qed. -Lemma weak_sep_openE : - @open T = @open weakT. +Lemma weak_sep_openE : @open T = @open weakT. Proof. -rewrite predeqE => A; split; rewrite ? openE => P z => /P. - by rewrite /= /interior weak_sep_nbhsE. -by rewrite /= /interior weak_sep_nbhsE. +rewrite predeqE => A; rewrite ?openE /interior. +by split => + z => /(_ z); rewrite weak_sep_nbhsE. Qed. -Definition join_product (x : weakT) : PU := fun i => f_ i x. +Definition join_product (x : T) : PU := fun i => f_ i x. Lemma join_product_continuous : continuous join_product. Proof. +suff : continuous (join_product : weakT -> PU). + by move=> cts x U => /cts; rewrite /= nbhs_simpl /= -weak_sep_nbhsE. move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). -move=> i; move: x. -apply/(@continuousP _ (weak_topologicalType _)) => A [B oB <-]. -rewrite (_ : @^~ i = prod_topo_apply i) //. +move=> i; move: x; apply/(@continuousP _ (weak_topologicalType _)) => A [B ? E]. +rewrite -E (_ : @^~ i = prod_topo_apply i) //. have -> : join_product @^-1` (prod_topo_apply i @^-1` B) = f_ i @^-1` B by []. -apply: open_comp => // + _; rewrite /cvg_to => x U //=. -rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. +apply: open_comp => // + _; rewrite /cvg_to => x U. +by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. Qed. -Lemma join_product_open : forall (A : set weakT), open A -> +Lemma join_product_open : forall (A : set T), open A -> open ((join_product @` A) : set (subspace (join_product @` setT))). Proof. -move=> A; rewrite -weak_sep_openE => oA. -have S := @sepf (~` A) _ (open_closedC oA). -rewrite openE => y /= [x Ax] jxy; rewrite /interior. -have [// | i nAfiy] := S x. +move=> A oA; rewrite openE => y /= [x Ax] jxy. +have [// | i nAfiy] := @sepf (~` A) x (open_closedC oA). pose B := prod_topo_apply i @^-1` (~` closure (f_ i @` ~` A)). apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). move=> z [[w ?]] wzE Bz; exists w => //. - move: Bz; rewrite /B -wzE /preimage /mkset closureC. - case=> K /= [oK KsubA] => /KsubA /=. + move: Bz; rewrite /B -wzE closureC; case=> K [oK KsubA] /KsubA. have -> : prod_topo_apply i (join_product w) = f_ i w by []. by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. apply: open_nbhs_nbhs; split; last by rewrite -jxy. apply: openI; first exact: open_subspaceT. -apply: open_subspaceW; apply: open_comp. +apply: open_subspaceW; apply: open_comp. by move=> + _; exact: prod_topo_apply_continuous. -by apply: closed_openC; exact: closed_closure. +by exact/closed_openC/closed_closure. Qed. Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product. @@ -6637,10 +6637,10 @@ apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. by apply subset_closure; exists y. Qed. -Lemma join_product_weak : accessible_space T -> - @open weakT = @open (weak_topologicalType join_product). +Lemma join_product_weak : set_inj [set: T] join_product -> + @open T = @open (weak_topologicalType join_product). Proof. -move=> /join_product_inj => inj; rewrite predeqE => U; split; first last. +move=> inj; rewrite predeqE => U; split; first last. by move=> [V ? <-]; apply open_comp => // + _; exact: join_product_continuous. move=> /join_product_open/open_subspaceP [V [oU VU]]. exists V => //; have := @f_equal _ _ (preimage join_product) _ _ VU. From ac42713d34e1f815c4c7b6a77c4d28cfe26ae735 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 10 Oct 2022 17:24:21 -0400 Subject: [PATCH 7/9] cleaning up proofs --- theories/topology.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 17f04bc25c..985924c0dd 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6601,7 +6601,7 @@ Definition join_product (x : T) : PU := fun i => f_ i x. Lemma join_product_continuous : continuous join_product. Proof. suff : continuous (join_product : weakT -> PU). - by move=> cts x U => /cts; rewrite /= nbhs_simpl /= -weak_sep_nbhsE. + by move=> cts x U => /cts; rewrite nbhs_simpl /= -weak_sep_nbhsE. move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). move=> i; move: x; apply/(@continuousP _ (weak_topologicalType _)) => A [B ? E]. rewrite -E (_ : @^~ i = prod_topo_apply i) //. @@ -6622,9 +6622,8 @@ apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). have -> : prod_topo_apply i (join_product w) = f_ i w by []. by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. apply: open_nbhs_nbhs; split; last by rewrite -jxy. -apply: openI; first exact: open_subspaceT. -apply: open_subspaceW; apply: open_comp. - by move=> + _; exact: prod_topo_apply_continuous. +apply: openI; first exact: open_subspaceT; apply: open_subspaceW. +apply: open_comp; first by move=> + _; exact: prod_topo_apply_continuous. by exact/closed_openC/closed_closure. Qed. From 70b9dc6f115967b7c84b280bb59d511c77abac6a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 26 Oct 2022 10:35:21 +0900 Subject: [PATCH 8/9] typos --- theories/topology.v | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 985924c0dd..423c452eb4 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -117,12 +117,12 @@ Require Import mathcomp_extra reals signed. (* predicates on natural numbers that are *) (* eventually true. *) (* separates_points_from_closed f == For a closed set U and point x outside *) -(* some member of the family `f` sends *) -(* f_i(x) outside (closure (f_i@` U)). *) -(* used together with `join_product` *) -(* join_product f == The function (x i => f i x). When the *) +(* some member of the family f sends *) +(* f_i(x) outside (closure (f_i @` U)). *) +(* Used together with join_product. *) +(* join_product f == The function (x => f ^~ x). When the *) (* family f separates points from closed *) -(* sets, join_product is an embedding *) +(* sets, join_product is an embedding. *) (* *) (* * Near notations and tactics: *) (* --> The purpose of the near notations and tactics is to make the *) @@ -3213,7 +3213,7 @@ Qed. Definition hausdorff_accessible : hausdorff_space T -> accessible_space. Proof. rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP]. -rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. +rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. by rewrite inE; apply: VUc; rewrite -inE. Qed. @@ -6542,21 +6542,20 @@ Qed. End SubspaceWeak. Definition separates_points_from_closed {I : Type} {T : topologicalType} - {U_ : I -> topologicalType} (f_ : forall i, (T -> U_ i)) := + {U_ : I -> topologicalType} (f_ : forall i, T -> U_ i) := forall (U : set T) x, closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x). -(* A handy technique for emebdding a space T into a product. The key interface - is 'separates_points_from_closed', which guarantees that the topologies +(* A handy technique for embedding a space T into a product. The key interface + is 'separates_points_from_closed', which guarantees that the topologies - T's native topology - sup (weak f_i) - the sup of all the weak topologies of f_i - weak (x => (f_1 x, f_2 x,...)) - the weak topology from the product space are equivalent (the last equivalence seems to require accessible_space). *) Section product_embeddings. -Context {I : choiceType} {T : topologicalType}. -Context {U_ : I -> topologicalType}. -Variable (f_ : forall i, (T -> U_ i)). +Context {I : choiceType} {T : topologicalType} {U_ : I -> topologicalType}. +Variable (f_ : forall i, T -> U_ i). Hypothesis sepf : separates_points_from_closed f_. Hypothesis ctsf : forall i, continuous (f_ i). @@ -6576,7 +6575,7 @@ move=> FF; split. move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [[oB ?]]]]. move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). apply: (wiFx i); have /= -> := @nbhsE (weak_topologicalType (f_ i)) x. -exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); repeat split => //. +exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); split; [split=>//|]. apply: open_comp; last by rewrite ?openC; last apply: closed_closure. by move=> + _; exact: weak_continuous. rewrite closureC preimage_bigcup => z [V [oV]] VnB => /VnB. @@ -6596,7 +6595,7 @@ rewrite predeqE => A; rewrite ?openE /interior. by split => + z => /(_ z); rewrite weak_sep_nbhsE. Qed. -Definition join_product (x : T) : PU := fun i => f_ i x. +Definition join_product (x : T) : PU := f_ ^~ x. Lemma join_product_continuous : continuous join_product. Proof. @@ -6610,21 +6609,22 @@ apply: open_comp => // + _; rewrite /cvg_to => x U. by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. Qed. -Lemma join_product_open : forall (A : set T), open A -> - open ((join_product @` A) : set (subspace (join_product @` setT))). +Lemma join_product_open (A : set T) : open A -> + open ((join_product @` A) : set (subspace (range join_product))). Proof. -move=> A oA; rewrite openE => y /= [x Ax] jxy. +move=> oA; rewrite openE => y /= [x Ax] jxy. have [// | i nAfiy] := @sepf (~` A) x (open_closedC oA). pose B := prod_topo_apply i @^-1` (~` closure (f_ i @` ~` A)). -apply: (@filterS _ _ _ ((join_product @` setT) `&` B)). +apply: (@filterS _ _ _ (range join_product `&` B)). move=> z [[w ?]] wzE Bz; exists w => //. move: Bz; rewrite /B -wzE closureC; case=> K [oK KsubA] /KsubA. have -> : prod_topo_apply i (join_product w) = f_ i w by []. by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT. apply: open_nbhs_nbhs; split; last by rewrite -jxy. -apply: openI; first exact: open_subspaceT; apply: open_subspaceW. -apply: open_comp; first by move=> + _; exact: prod_topo_apply_continuous. -by exact/closed_openC/closed_closure. +apply: openI; first exact: open_subspaceT. +apply: open_subspaceW; apply: open_comp. + by move=> + _; exact: prod_topo_apply_continuous. +exact/closed_openC/closed_closure. Qed. Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product. From 0e639029ceb6ce6a6bcdf7cafd05f55c577c47a7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 26 Oct 2022 17:18:03 +0900 Subject: [PATCH 9/9] display for open? --- theories/topology.v | 233 ++++++++++++++++++++++++-------------------- 1 file changed, 130 insertions(+), 103 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 423c452eb4..7b872ec19e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1555,6 +1555,11 @@ End PrincipalFilters. (** * Topological spaces *) +Inductive topology_display := default_topology_display. +Declare Scope topology_display_scope. +Delimit Scope topology_display_scope with tdisp. +Bind Scope topology_display_scope with topology_display. + Module Topological. Record mixin_of (T : Type) (nbhs : T -> set (set T)) := Mixin { @@ -1572,12 +1577,12 @@ Record class_of (T : Type) := Class { Section ClassDef. -Structure type := Pack { sort; _ : class_of sort }. +Structure type (disp : topology_display) := Pack { sort; _ : class_of sort }. Local Coercion sort : type >-> Sortclass. -Variables (T : Type) (cT : type). +Variables (T : Type) (disp : topology_display) (cT : type disp). Definition class := let: Pack _ c := cT return class_of cT in c. -Definition clone c of phant_id class c := @Pack T c. +Definition clone c of phant_id class c := @Pack disp T c. Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Local Coercion base : class_of >-> Filtered.class_of. @@ -1586,7 +1591,7 @@ Local Coercion mixin : class_of >-> mixin_of. Definition pack nbhs' (m : @mixin_of T nbhs') := fun bT (b : Filtered.class_of T T) of phant_id (@Filtered.class T bT) b => fun m' of phant_id m (m' : @mixin_of T (Filtered.nbhs_op b)) => - @Pack T (@Class _ b m'). + @Pack disp T (@Class _ b m'). Definition eqType := @Equality.Pack cT xclass. Definition choiceType := @Choice.Pack cT xclass. @@ -1609,11 +1614,11 @@ Canonical pointedType. Coercion filteredType : type >-> Filtered.type. Canonical filteredType. Notation topologicalType := type. -Notation TopologicalType T m := (@pack T _ m _ _ idfun _ idfun). +Notation TopologicalType disp T m := (@pack T disp _ m _ _ idfun _ idfun). Notation TopologicalMixin := Mixin. -Notation "[ 'topologicalType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) +Notation "[ 'topologicalType' 'of' T 'for' cT ]" := (@clone T _ cT _ idfun) (at level 0, format "[ 'topologicalType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'topologicalType' 'of' T ]" := (@clone T _ _ id) +Notation "[ 'topologicalType' 'of' T ]" := (@clone T _ _ _ id) (at level 0, format "[ 'topologicalType' 'of' T ]") : form_scope. End Exports. @@ -1624,7 +1629,7 @@ Export Topological.Exports. Section Topological1. -Context {T : topologicalType}. +Context {disp : _} {T : topologicalType disp}. Definition open := Topological.open (Topological.class T). @@ -1726,7 +1731,7 @@ Proof. by move=> [Aop Ap] [Bop Bp]; split; [apply: openI|split]. Qed. Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A. Proof. by rewrite nbhsE => p_A; exists A; split. Qed. -Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°. +Lemma interiorI (A B : set T): (A `&` B)^° = A^° `&` B^°. Proof. rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 [?]] | []]. - by rewrite subsetI => // -[? ?]; split; exists B0. @@ -1740,7 +1745,11 @@ Notation "A ^°" := (interior A) : classical_set_scope. Notation continuous f := (forall x, f%function @ x --> f%function x). -Lemma continuousP (S T : topologicalType) (f : S -> T) : +(* TODO: move *) +Reserved Notation "d .-open" (at level 2, format "d .-open"). +Notation "d .-open" := (@open d%tdisp) : classical_set_scope. + +Lemma continuousP d1 d2 (S : topologicalType d1) (T : topologicalType d2) (f : S -> T) : continuous f <-> forall A, open A -> open (f @^-1` A). Proof. split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont. @@ -1748,28 +1757,29 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [[Bop Bfs] sBA]]. by exists (f @^-1` B); split; [split=> //; apply/fcont|move=> ? /sBA]. Qed. -Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x : +Lemma continuous_comp d1 d2 d3 (R : topologicalType d1) (S : topologicalType d2) + (T : topologicalType d3) (f : R -> S) (g : S -> T) x : {for x, continuous f} -> {for (f x), continuous g} -> {for x, continuous (g \o f)}. Proof. exact: cvg_comp. Qed. -Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : +Lemma open_comp {d1 d2} {T : topologicalType d1} {U : topologicalType d2} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D). Proof. rewrite !openE => fcont Dop x /= Dfx. by apply: fcont; [rewrite inE|apply: Dop]. Qed. -Lemma cvg_fmap {T: topologicalType} {U : topologicalType} +Lemma cvg_fmap {d1 d2} {T : topologicalType d1} {U : topologicalType d2} (F : set (set T)) x (f : T -> U) : {for x, continuous f} -> F --> x -> f @ F --> f x. Proof. by move=> cf fx P /cf /fx. Qed. -Lemma near_join (T : topologicalType) (x : T) (P : set T) : +Lemma near_join d (T : topologicalType d) (x : T) (P : set T) : (\near x, P x) -> \near x, \near x, P x. Proof. exact: nbhs_interior. Qed. -Lemma near_bind (T : topologicalType) (P Q : set T) (x : T) : +Lemma near_bind d (T : topologicalType d) (P Q : set T) (x : T) : (\near x, (\near x, P x) -> Q x) -> (\near x, P x) -> \near x, Q x. Proof. move=> PQ xP; near=> y; apply: (near PQ y) => //; @@ -1778,7 +1788,7 @@ Unshelve. all: by end_near. Qed. (* limit composition *) -Lemma continuous_cvg {T : Type} {V U : topologicalType} +Lemma continuous_cvg {T : Type} {d1 d2} {V : topologicalType d1} {U : topologicalType d2} (F : set (set T)) (FF : Filter F) (f : T -> V) (h : V -> U) (a : V) : {for a, continuous h} -> @@ -1788,8 +1798,9 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (@cvg_comp _ _ _ _ h _ _ _ fa). Qed. -Lemma continuous_is_cvg {T : Type} {V U : topologicalType} [F : set (set T)] - (FF : Filter F) (f : T -> V) (h : V -> U) : +Lemma continuous_is_cvg {T : Type} {d1 d2} {V : topologicalType d1} + {U : topologicalType d2} [F : set (set T)] (FF : Filter F) (f : T -> V) + (h : V -> U) : (forall l, f x @[x --> F] --> l -> {for l, continuous h}) -> cvg (f x @[x --> F]) -> cvg ((h \o f) x @[x --> F]). Proof. @@ -1797,7 +1808,7 @@ move=> ach /cvg_ex[l fxl]; apply/cvg_ex; exists (h l). by apply: continuous_cvg => //; exact: ach. Qed. -Lemma continuous2_cvg {T : Type} {V W U : topologicalType} +Lemma continuous2_cvg {T : Type} {d1 d2 d3} {V : topologicalType d1} {W : topologicalType d2} {U : topologicalType d3} (F : set (set T)) (FF : Filter F) (f : T -> V) (g : T -> W) (h : V -> W -> U) (a : V) (b : W) : h z.1 z.2 @[z --> (a, b)] --> h a b -> @@ -1807,50 +1818,50 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (@cvg_comp _ _ _ _ (fun x => h x.1 x.2) _ _ _ (cvg_pair fa fb)). Qed. -Lemma cvg_near_cst (T : Type) (U : topologicalType) +Lemma cvg_near_cst (T : Type) d (U : topologicalType d) (l : U) (f : T -> U) (F : set (set T)) {FF : Filter F} : (\forall x \near F, f x = l) -> f @ F --> l. Proof. move=> fFl P /=; rewrite !near_simpl => Pl. by apply: filterS fFl => _ ->; apply: nbhs_singleton. Qed. -Arguments cvg_near_cst {T U} l {f F FF}. +Arguments cvg_near_cst {T d U} l {f F FF}. -Lemma is_cvg_near_cst (T : Type) (U : topologicalType) +Lemma is_cvg_near_cst (T : Type) d (U : topologicalType d) (l : U) (f : T -> U) (F : set (set T)) {FF : Filter F} : (\forall x \near F, f x = l) -> cvg (f @ F). Proof. by move=> /cvg_near_cst/cvgP. Qed. -Arguments is_cvg_near_cst {T U} l {f F FF}. +Arguments is_cvg_near_cst {T d U} l {f F FF}. -Lemma near_cst_continuous (T U : topologicalType) +Lemma near_cst_continuous d1 d2 (T : topologicalType d1) (U : topologicalType d2) (l : U) (f : T -> U) (x : T) : (\forall y \near x, f y = l) -> {for x, continuous f}. Proof. move=> eq_f_l; apply: cvg_near_cst; apply: filterS (eq_f_l) => y ->. by rewrite (nbhs_singleton eq_f_l). Qed. -Arguments near_cst_continuous {T U} l [f x]. +Arguments near_cst_continuous {d1 d2 T U} l [f x]. -Lemma cvg_cst (U : topologicalType) (x : U) (T : Type) +Lemma cvg_cst d (U : topologicalType d) (x : U) (T : Type) (F : set (set T)) {FF : Filter F} : (fun _ : T => x) @ F --> x. Proof. by apply: cvg_near_cst; near=> x0. Unshelve. all: by end_near. Qed. -Arguments cvg_cst {U} x {T F FF}. +Arguments cvg_cst {d U} x {T F FF}. #[global] Hint Resolve cvg_cst : core. -Lemma is_cvg_cst (U : topologicalType) (x : U) (T : Type) +Lemma is_cvg_cst d (U : topologicalType d) (x : U) (T : Type) (F : set (set T)) {FF : Filter F} : cvg ((fun _ : T => x) @ F). Proof. by apply: cvgP; apply: cvg_cst. Qed. -Arguments is_cvg_cst {U} x {T F FF}. +Arguments is_cvg_cst {d U} x {T F FF}. #[global] Hint Resolve is_cvg_cst : core. -Lemma cst_continuous {T U : topologicalType} (x : U) : +Lemma cst_continuous {d1 d2} {T : topologicalType d1} {U : topologicalType d2} (x : U) : continuous (fun _ : T => x). Proof. by move=> t; apply: cvg_cst. Qed. Section within_topologicalType. -Context {T : topologicalType} (A : set T). +Context {d : _} {T : topologicalType d} (A : set T). Implicit Types B : set T. (* Relation between globally and within A (nbhs x) *) @@ -1895,7 +1906,7 @@ move=> [V FV AU]; rewrite /within /prop_near1 nbhs_simpl; near=> w => Aw. by have []// : (U `&` A) w; rewrite AU; split => //; apply: (near FV). Unshelve. all: by end_near. Qed. -Lemma fmap_within_eq {S : topologicalType} (F : set (set T)) (f g : T -> S) : +Lemma fmap_within_eq {d2} {S : topologicalType d2} (F : set (set T)) (f g : T -> S) : Filter F -> {in A, f =1 g} -> f @ within A F --> g @ within A F. Proof. move=> FF feq U /=; near_simpl; apply: filter_app. @@ -1904,7 +1915,7 @@ exact: (near (withinT A FF) w). Unshelve. all: by end_near. Qed. End within_topologicalType. -Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). +Notation "[ 'locally' P ]" := (@locally_of _ _ _ _ (Phantom _ P)). (** ** Topology defined by a filter *) @@ -2083,7 +2094,7 @@ Proof. by move=> i j t _ _ -> ->; exists j. Qed. Definition nat_topologicalTypeMixin := topologyOfBaseMixin bT bD. Canonical nat_filteredType := FilteredType nat nat (nbhs_of_open (open_from D b)). -Canonical nat_topologicalType := TopologicalType nat nat_topologicalTypeMixin. +Canonical nat_topologicalType d := TopologicalType d nat nat_topologicalTypeMixin. End nat_topologicalType. @@ -2149,9 +2160,22 @@ Proof. case=> N _ NPS; exists (S N) => // [[]]; rewrite /= ?ltn0 //. Qed. (** ** Topology on the product of two spaces *) +Definition topology_prod_display : + (topology_display * topology_display) -> topology_display. +Proof. exact. Qed. + +(* TODO: move *) +Reserved Notation "p .-prod" (at level 1, format "p .-prod"). +Reserved Notation "p .-prod.-open" + (at level 2, format "p .-prod.-open"). +Notation "p .-prod" := (topology_prod_display p) : classical_set_scope. +Notation "p .-prod.-open" := + ((p.-prod).-open : set (set (_ * _))) : + classical_set_scope. + Section Prod_Topology. -Context {T U : topologicalType}. +Context {d1 d2} {T : topologicalType d1} {U : topologicalType d2}. Let prod_nbhs (p : T * U) := filter_prod (nbhs p.1) (nbhs p.2). @@ -2174,7 +2198,7 @@ Definition prod_topologicalTypeMixin := topologyOfFilterMixin prod_nbhs_filter prod_nbhs_singleton prod_nbhs_nbhs. Canonical prod_topologicalType := - TopologicalType (T * U) prod_topologicalTypeMixin. + TopologicalType (topology_prod_display (d1, d2)) (T * U) prod_topologicalTypeMixin. End Prod_Topology. @@ -2182,7 +2206,7 @@ End Prod_Topology. Section matrix_Topology. -Variables (m n : nat) (T : topologicalType). +Variables (m n : nat) (d : _) (T : topologicalType d). Implicit Types M : 'M[T]_(m, n). @@ -2209,8 +2233,8 @@ Qed. Definition matrix_topologicalTypeMixin := topologyOfFilterMixin mx_nbhs_filter mx_nbhs_singleton mx_nbhs_nbhs. -Canonical matrix_topologicalType := - TopologicalType 'M[T]_(m, n) matrix_topologicalTypeMixin. +Canonical matrix_topologicalType d := + TopologicalType d 'M[T]_(m, n) matrix_topologicalTypeMixin. End matrix_Topology. @@ -2218,7 +2242,7 @@ End matrix_Topology. Section Weak_Topology. -Variable (S : pointedType) (T : topologicalType) (f : S -> T). +Variable (S : pointedType) (d : _) (T : topologicalType d) (f : S -> T). Definition wopen := [set f @^-1` A | A in open]. @@ -2247,20 +2271,20 @@ Qed. Definition weak_topologicalTypeMixin := topologyOfOpenMixin wopT wopI wop_bigU. Let S_filteredClass := Filtered.Class (Pointed.class S) (nbhs_of_open wopen). -Definition weak_topologicalType := - Topological.Pack (@Topological.Class _ S_filteredClass +Definition weak_topologicalType d := + Topological.Pack d (@Topological.Class _ S_filteredClass weak_topologicalTypeMixin). -Lemma weak_continuous : continuous (f : weak_topologicalType -> T). +Lemma weak_continuous : continuous (f : weak_topologicalType d -> T). Proof. by apply/continuousP => A ?; exists A. Qed. Lemma cvg_image (F : set (set S)) (s : S) : Filter F -> f @` setT = setT -> - F --> (s : weak_topologicalType) <-> [set f @` A | A in F] --> f s. + F --> (s : weak_topologicalType d) <-> [set f @` A | A in F] --> f s. Proof. move=> FF fsurj; split=> [cvFs|cvfFfs]. move=> A /weak_continuous [B [Bop [Bs sBAf]]]. - have /cvFs FB : nbhs (s : weak_topologicalType) B by apply: open_nbhs_nbhs. + have /cvFs FB : nbhs (s : weak_topologicalType d) B by apply: open_nbhs_nbhs. rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. exact: image_preimage. move=> A /= [_ [[B Bop <-] [Bfs sBfA]]]. @@ -2277,27 +2301,27 @@ Section Sup_Topology. Variable (T : pointedType) (I : Type) (Tc : I -> Topological.class_of T). -Let TS := fun i => Topological.Pack (Tc i). +Let TS d := fun i => Topological.Pack d (Tc i). -Definition sup_subbase := \bigcup_i (@open (TS i) : set (set T)). +Definition sup_subbase d := \bigcup_i (@open d (TS d i) : set (set T)). -Definition sup_topologicalTypeMixin := topologyOfSubbaseMixin sup_subbase id. +Definition sup_topologicalTypeMixin d := topologyOfSubbaseMixin (sup_subbase d) id. -Definition sup_topologicalType := - Topological.Pack (@Topological.Class _ (Filtered.Class (Pointed.class T) _) - sup_topologicalTypeMixin). +Definition sup_topologicalType d := + Topological.Pack d (@Topological.Class _ (Filtered.Class (Pointed.class T) _) + (sup_topologicalTypeMixin d)). -Lemma cvg_sup (F : set (set T)) (t : T) : - Filter F -> F --> (t : sup_topologicalType) <-> forall i, F --> (t : TS i). +Lemma cvg_sup d (F : set (set T)) (t : T) : + Filter F -> F --> (t : sup_topologicalType d) <-> forall i, F --> (t : TS d i). Proof. move=> Ffilt; split=> cvFt. - move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [[Bop Bt] sBA]]. + move=> i A /=; rewrite (@nbhsE d (TS d i)) => - [B [[Bop Bt] sBA]]. apply: cvFt; exists B; split=> //; exists [set B]; last first. by rewrite predeqE => ?; split=> [[_ ->]|] //; exists B. move=> _ ->; exists [fset B]%fset. by move=> ?; rewrite inE inE => /eqP->; exists i. by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->. -move=> A /=; rewrite (@nbhsE sup_topologicalType). +move=> A /=; rewrite (@nbhsE d (sup_topologicalType d)). move=> [_ [[[B sB <-] [C BC Ct]] sUBA]]. rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C). by move=> ??; exists C. @@ -2312,21 +2336,21 @@ End Sup_Topology. Section Product_Topology. -Variable (I : Type) (T : I -> topologicalType). +Variable (I : Type) (d : _) (T : I -> topologicalType d). Definition product_topologicalType := sup_topologicalType (fun i => Topological.class - (weak_topologicalType (fun f : dep_arrow_pointedType T => f i))). + (weak_topologicalType (fun f : dep_arrow_pointedType T => f i) d)). End Product_Topology. (** dnbhs *) -Definition dnbhs {T : topologicalType} (x : T) := +Definition dnbhs {d} {T : topologicalType d} (x : T) := within (fun y => y != x) (nbhs x). Notation "x ^'" := (dnbhs x) : classical_set_scope. -Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x. +Lemma dnbhsE d (T : topologicalType d) (x : T) : nbhs x = x^' `&` at_point x. Proof. rewrite predeqE => A; split=> [x_A|[x_A Ax]]. split; last exact: nbhs_singleton. @@ -2336,11 +2360,11 @@ move: x_A; rewrite /dnbhs !nbhsE => -[B [x_B sBA]]; exists B. by split=> // y /sBA Ay; case: (eqVneq y x) => [->|]. Qed. -Global Instance dnbhs_filter {T : topologicalType} (x : T) : Filter x^'. +Global Instance dnbhs_filter {d} {T : topologicalType d} (x : T) : Filter x^'. Proof. exact: within_filter. Qed. #[global] Typeclasses Opaque dnbhs. -Canonical dnbhs_filter_on (T : topologicalType) (x : T) := +Canonical dnbhs_filter_on d (T : topologicalType d) (x : T) := FilterType x^' (dnbhs_filter _). Lemma cvg_fmap2 (T U : Type) (f : T -> U): @@ -2351,23 +2375,23 @@ Lemma cvg_within_filter {T U} {f : T -> U} (F : set (set T)) {FF : (Filter F) } (G : set (set U)) : forall (D : set T), (f @ F) --> G -> (f @ within D F) --> G. Proof. move=> ?; exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed. -Lemma cvg_app_within {T} {U : topologicalType} (f : T -> U) (F : set (set T)) +Lemma cvg_app_within {T} d {U : topologicalType d} (f : T -> U) (F : set (set T)) (D : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F). Proof. by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_filter. Qed. -Lemma nbhs_dnbhs {T : topologicalType} (x : T) : x^' `=>` nbhs x. +Lemma nbhs_dnbhs {d} {T : topologicalType d} (x : T) : x^' `=>` nbhs x. Proof. exact: cvg_within. Qed. (** meets *) -Lemma meets_openr {T : topologicalType} (F : set (set T)) (x : T) : +Lemma meets_openr {d} {T : topologicalType d} (F : set (set T)) (x : T) : F `#` nbhs x = F `#` open_nbhs x. Proof. rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|]. by move=> P A B {}/P P; rewrite nbhsE => -[B' [/P + sB]]; apply: subsetI_neq0. Qed. -Lemma meets_openl {T : topologicalType} (F : set (set T)) (x : T) : +Lemma meets_openl {d} {T : topologicalType d} (F : set (set T)) (x : T) : nbhs x `#` F = open_nbhs x `#` F. Proof. by rewrite meetsC meets_openr meetsC. Qed. @@ -2398,7 +2422,7 @@ Proof. by rewrite meetsxx; apply: filter_not_empty. Qed. Section Closed. -Context {T : topologicalType}. +Context {d : _} {T : topologicalType d}. Definition closure (A : set T) := [set p : T | forall B, nbhs p B -> A `&` B !=set0]. @@ -2502,7 +2526,7 @@ Proof. by move=> p clclAp B /nbhs_interior /clclAp [q [clAq /clAq]]. Qed. End Closed. -Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) : +Lemma closed_comp d {T U : topologicalType d} (f : T -> U) (D : set U) : {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D). Proof. rewrite !closedE=> f_continuous D_cl x /= xDf. @@ -2512,7 +2536,7 @@ have NDfx : ~ D (f x). by apply: f_continuous fxD; rewrite inE. Qed. -Lemma closed_cvg {T} {V : topologicalType} {F} {FF : ProperFilter F} +Lemma closed_cvg {T} {d} {V : topologicalType d} {F} {FF : ProperFilter F} (u_ : T -> V) (A : V -> Prop) : (* BUG: elim does not see this as an elimination principle if A : set V *) closed A -> (\forall n \near F, A (u_ n)) -> @@ -2521,9 +2545,10 @@ Proof. move=> + FAu_ l u_Fl; apply => B /u_Fl /=; rewrite nbhs_filterE. by move=> /(filterI FAu_) => /filter_ex[t [Au_t u_Bt]]; exists (u_ t). Qed. -Arguments closed_cvg {T V F FF u_} _ _ _ _ _. +Arguments closed_cvg {T d V F FF u_} _ _ _ _ _. -Lemma continuous_closedP (S T : topologicalType) (f : S -> T) : +Lemma continuous_closedP d1 d2 (S : topologicalType d1) (T : topologicalType d2) + (f : S -> T) : continuous f <-> forall A, closed A -> closed (f @^-1` A). Proof. rewrite continuousP; split=> ctsf ? ?. @@ -2531,12 +2556,12 @@ rewrite continuousP; split=> ctsf ? ?. by rewrite -closedC preimage_setC; apply ctsf; rewrite closedC. Qed. -Lemma closedU (T : topologicalType) (D E : set T) : +Lemma closedU d (T : topologicalType d) (D E : set T) : closed D -> closed E -> closed (D `|` E). Proof. by rewrite -?openC setCU; exact: openI. Qed. Section closure_lemmas. -Variable T : topologicalType. +Variables (d : _) (T : topologicalType d). Implicit Types E A B U : set T. Lemma closure_subset A B : A `<=` B -> closure A `<=` closure B. @@ -2545,7 +2570,7 @@ Proof. by move=> ? ? CAx ?; move/CAx; exact/subsetI_neq0. Qed. Lemma closureE A : closure A = smallest closed A. Proof. rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closure_subset AB). -exact: (smallest_sub (@closed_closure _ _) (@subset_closure _ _)). +exact: (smallest_sub (@closed_closure _ _ _) (@subset_closure _ _ _)). Qed. Lemma closureC E : @@ -2568,7 +2593,7 @@ End closure_lemmas. Section Compact. -Context {T : topologicalType}. +Context {d : _} {T : topologicalType d}. Definition cluster (F : set (set T)) := [set p : T | F `#` nbhs p]. @@ -2663,7 +2688,7 @@ End Compact. Arguments hausdorff_space : clear implicits. Section near_covering. -Context {X : topologicalType}. +Context {d : _} {X : topologicalType d}. Definition near_covering (K : set X) := forall (I : Type) (F : set (set I)) (P : I -> X -> Prop), @@ -2725,7 +2750,7 @@ Class UltraFilter T (F : set (set T)) := { max_filter : forall G : set (set T), ProperFilter G -> F `<=` G -> G = F }. -Lemma ultra_cvg_clusterE (T : topologicalType) (F : set (set T)) : +Lemma ultra_cvg_clusterE d (T : topologicalType d) (F : set (set T)) : UltraFilter F -> cluster F = [set p | F --> p]. Proof. move=> FU; rewrite predeqE => p; split. @@ -2768,7 +2793,7 @@ move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H. exact: filterS HB. Qed. -Lemma compact_ultra (T : topologicalType) : +Lemma compact_ultra d (T : topologicalType d) : compact = [set A | forall F : set (set T), UltraFilter F -> F A -> A `&` [set p | F --> p] !=set0]. Proof. @@ -2848,10 +2873,10 @@ rewrite preimage_setC image_preimage // => GnA. by have /filter_ex [? []] : G (A `&` (~` A)) by apply: filterI. Qed. -Lemma tychonoff (I : eqType) (T : I -> topologicalType) +Lemma tychonoff (I : eqType) d (T : I -> topologicalType d) (A : forall i, set (T i)) : (forall i, compact (A i)) -> - @compact (product_topologicalType T) + @compact d (product_topologicalType T d) [set f : forall i, T i | forall i, A i (f i)]. Proof. move=> Aco; rewrite compact_ultra => F FU FA. @@ -2887,7 +2912,7 @@ End Tychonoff. Section Precompact. -Context {X : topologicalType}. +Context {d : _} {X : topologicalType d}. Lemma compactU (A B : set X) : compact A -> compact B -> compact (A `|` B). Proof. @@ -2921,7 +2946,7 @@ by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB. Qed. Lemma compact_precompact (A B : set X) : - hausdorff_space X -> compact A -> precompact A. + hausdorff_space d X -> compact A -> precompact A. Proof. move=> h c; rewrite precompactE ( _ : closure A = A)//. apply/esym/closure_id; exact: compact_closed. @@ -2939,12 +2964,12 @@ Definition locally_compact (A : set X) := [locally precompact A]. End Precompact. Section Product_Hausdorff. -Context {X : choiceType} {K : X -> topologicalType}. +Context {X : choiceType} {d : _} {K : X -> topologicalType d}. (* This a helper function to prove products preserve hausdorff. In particular *) (* we use its continuity turn clustering in `product_topologicalType K` to *) (* clustering in K x for each X. *) -Definition prod_topo_apply x (f : product_topologicalType K) := f x. +Definition prod_topo_apply x (f : @product_topologicalType _ _ K d) := f x. Lemma prod_topo_applyE x f : prod_topo_apply x f = f x. Proof. by []. Qed. @@ -2964,7 +2989,7 @@ by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image. Qed. Lemma hausdorff_product : - (forall x, hausdorff_space (K x)) -> hausdorff_space (@product_topologicalType X K). + (forall x, hausdorff_space d (K x)) -> hausdorff_space d (@product_topologicalType X _ K d). Proof. move=> hsdfK p q /= clstr; apply: functional_extensionality_dep => x. apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]]. @@ -3011,7 +3036,7 @@ Definition finSubCover (I : choiceType) (D : set I) Section Covers. -Variable T : topologicalType. +Variables (d : _) (T : topologicalType d). Definition cover_compact (A : set T) := forall (I : choiceType) (D : set I) (f : I -> set T), @@ -3114,7 +3139,7 @@ Qed. End Covers. Section separated_topologicalType. -Variable (T : topologicalType). +Variables (d : _) (T : topologicalType d). Implicit Types x y : T. Local Open Scope classical_set_scope. @@ -3190,7 +3215,7 @@ by rewrite fmapiE; apply: filterS => x [y []]; exists y. Unshelve. all: by end_near. Qed. Definition cvg_toi_locally_close := @cvgi_close. -Lemma open_hausdorff : hausdorff_space T = +Lemma open_hausdorff : hausdorff_space d T = forall x y, x != y -> exists2 AB, (x \in AB.1 /\ y \in AB.2) & [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0]. @@ -3210,14 +3235,14 @@ move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)). by rewrite -set0P => /(_ _ _)/negP; apply. Qed. -Definition hausdorff_accessible : hausdorff_space T -> accessible_space. +Definition hausdorff_accessible : hausdorff_space d T -> accessible_space. Proof. rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP]. rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //. by rewrite inE; apply: VUc; rewrite -inE. Qed. -Hypothesis sep : hausdorff_space T. +Hypothesis sep : hausdorff_space d T. Lemma closeE x y : close x y = (x = y). Proof. @@ -3266,7 +3291,7 @@ Qed. End separated_topologicalType. Section connected_sets. -Variable T : topologicalType. +Variables (d : _) (T : topologicalType d). Implicit Types A B C D : set T. Definition connected A := @@ -3296,12 +3321,12 @@ rewrite -propeqE; apply notLR; rewrite propeqE. split=> [conE [E [E0 EU [E1 E2]]]|conE B B0 [C oC BAC] [D cD BAD]]. suff : E true = A. move/esym/(congr1 (setD^~ (closure (E true)))); rewrite EU setDUl. - have := @subset_closure _ (E true); rewrite -setD_eq0 => ->; rewrite setU0. + have := @subset_closure _ _ (E true); rewrite -setD_eq0 => ->; rewrite setU0. by move/setDidPl : E2 => ->; exact/eqP/set0P. apply: (conE _ (E0 true)). - exists (~` (closure (E false))); first exact/closed_openC/closed_closure. rewrite EU setIUl. - have /subsets_disjoint -> := @subset_closure _ (E false); rewrite set0U. + have /subsets_disjoint -> := @subset_closure _ _ (E false); rewrite set0U. by apply/esym/setIidPl/disjoints_subset; rewrite setIC. - exists (closure (E true)); first exact: closed_closure. by rewrite EU setIUl E2 set0U; exact/esym/setIidPl/subset_closure. @@ -3315,7 +3340,7 @@ exists (fun i => if i is false then A `\` C else A `&` C); split. + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?]. by exists C => //; split=> //; rewrite setDE setCI setCK; right. + apply/disjoints_subset => y -[Ay Cy]. - rewrite -BAC BAD=> /closureI[_]; rewrite -(proj1 (@closure_id _ _) cD)=> Dy. + rewrite -BAC BAD=> /closureI[_]; rewrite -(proj1 (@closure_id _ _ _) cD)=> Dy. by have : B y; [by rewrite BAD; split|rewrite BAC => -[]]. Qed. @@ -3364,7 +3389,7 @@ wlog E0c : E E0 EU sE / E false c. by apply: (G (E \o negb)) => //; [case => /=|rewrite EU setUC|rewrite separatedC]. move: (E0 true) => /set0P/eqP; apply. -have [/eqP //|/set0P[d E1d]] := boolP (E true == set0). +have [/eqP //|/set0P[d' E1d']] := boolP (E true == set0). have : \bigcup_(i in P) A i `<=` E false. suff AE : forall i, P i -> A i `<=` E false by move=> x [j ? ?]; exact: (AE j). move=> j Pj. @@ -3372,8 +3397,8 @@ have : \bigcup_(i in P) A i `<=` E false. rewrite -EU => /(_ (bigcup_sup _) (cA _ Pj)) [//| | AjE1]; first exact. exfalso; have E1c := AjE1 _ (AIc _ Pj). by move/separated_disjoint : sE; apply/eqP/set0P; exists c. -rewrite EU subUset => -[_] /(_ _ E1d) E0d; exfalso. -by move/separated_disjoint : sE; apply/eqP/set0P; exists d. +rewrite EU subUset => -[_] /(_ _ E1d') E0d; exfalso. +by move/separated_disjoint : sE; apply/eqP/set0P; exists d'. Qed. Lemma connectedU A B : A `&` B !=set0 -> connected A -> connected B -> @@ -3438,8 +3463,8 @@ by apply: connected_component_sym. Qed. End connected_sets. -Arguments connected {T}. -Arguments connected_component {T}. +Arguments connected {d T}. +Arguments connected_component {d T}. Section DiscreteTopology. Section DiscreteMixin. @@ -3457,10 +3482,10 @@ Definition discrete_topological_mixin := End DiscreteMixin. -Definition discrete_space (X : topologicalType) := +Definition discrete_space d (X : topologicalType d) := @nbhs X _ = @principal_filter X. -Context {X : topologicalType} {dsc: discrete_space X}. +Context {d : _} {X : topologicalType d} {dsc : discrete_space X}. Lemma discrete_open (A : set X) : open A. Proof. @@ -3480,13 +3505,13 @@ rewrite /filter_of dsc nbhs_simpl; split; first by exact. by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->. Qed. -Lemma discrete_hausdorff : hausdorff_space X. +Lemma discrete_hausdorff : hausdorff_space d X. Proof. by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q))[x [] -> ->]. Qed. -Canonical bool_discrete_topology : topologicalType := - TopologicalType bool discrete_topological_mixin. +Canonical bool_discrete_topology : topologicalType d := + TopologicalType d bool discrete_topological_mixin. Lemma discrete_bool : discrete_space bool_discrete_topology. Proof. by []. Qed. @@ -3498,6 +3523,8 @@ End DiscreteTopology. #[global] Hint Resolve discrete_bool : core. +xxx + (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.