From 8f5020c5ad085dfeebe1a3006cb583e4217e7a3a Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Wed, 5 Oct 2022 20:12:57 -0400
Subject: [PATCH 01/16] swapping machines

---
 theories/topology.v | 81 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 81 insertions(+)

diff --git a/theories/topology.v b/theories/topology.v
index dfba897265..3b883687fc 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3666,6 +3666,85 @@ by move=> ->; have := projT2 (sigW (npts N)).
 Qed.
 
 End perfect_sets.
+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 *)
 
@@ -6886,6 +6965,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 b077c1f4bb127680416d67a609556b63141e485c Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 00:45:08 -0400
Subject: [PATCH 02/16] 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 3b883687fc..7035ee0646 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3671,79 +3671,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 *)
@@ -6861,6 +6788,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.
@@ -6965,8 +6979,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 fcdaeffa9a7d36d5a4c04b05c0dca0edc56565e1 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 11:10:08 -0400
Subject: [PATCH 03/16] hausdorff accessible

---
 theories/topology.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/topology.v b/theories/topology.v
index 7035ee0646..b4d7df950d 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3334,6 +3334,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).
@@ -6873,6 +6880,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 44ffa1663f653d1ea935deb412b2bfda1b8d4244 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 13:46:11 -0400
Subject: [PATCH 04/16] 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 b4d7df950d..dbb1a589c1 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6873,26 +6873,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 687de136bd8b2d70dbae5a3b18508840c722062d Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 14:13:08 -0400
Subject: [PATCH 05/16] changelog

---
 CHANGELOG_UNRELEASED.md    | 136 +++++++++++++++++++++++++++++++++++++
 classical/classical_sets.v |   3 +
 theories/topology.v        |  27 ++++----
 3 files changed, 153 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 30570d33e4..c6a96b377b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -63,6 +63,142 @@
 - in `constructive_ereal.v`:
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`
   + lemma `fin_num_sume_distrr`
+  + lemmas `set_compose_subset`, `compose_diag`
+  + notation `\;` for the composition of relations
+- OPAM package `coq-mathcomp-classical` containing `boolp.v`
+- file `all_classical.v`
+- in file `mathcomp_extra.v`:
+  + lemmas `pred_oappE` and `pred_oapp_set` (from `classical_sets.v`)
+  + lemma `sumr_le0`
+- in file `fsbigop.v`:
+  + lemmas `fsumr_ge0`, `fsumr_le0`, `fsumr_gt0`, `fsumr_lt0`, `pfsumr_eq0`,
+    `pair_fsbig`, `exchange_fsbig`
+- in file `ereal.v`:
+  + notation `\sum_(_ \in _) _` (from `fsbigop.v`)
+  + lemmas `fsume_ge0`, `fsume_le0`, `fsume_gt0`, `fsume_lt0`,
+    `pfsume_eq0`, `lee_fsum_nneg_subset`, `lee_fsum`,
+    `ge0_mule_fsumr`, `ge0_mule_fsuml` (from `fsbigop.v`)
+  + lemmas `finite_supportNe`, `dual_fsumeE`, `dfsume_ge0`, `dfsume_le0`,
+    `dfsume_gt0`, `dfsume_lt0`, `pdfsume_eq0`, `le0_mule_dfsumr`, `le0_mule_dfsuml`
+- file `classical/set_interval.v`
+- in file `classical/set_interval.v`:
+  + definitions `neitv`, `set_itv_infty_set0`, `set_itvE`,
+    `disjoint_itv`, `conv`, `factor`, `ndconv` (from `set_interval.v`)
+  + lemmas `neitv_lt_bnd`, `set_itvP`, `subset_itvP`, `set_itvoo`, `set_itv_cc`,
+    `set_itvco`, `set_itvoc`, `set_itv1`, `set_itvoo0`, `set_itvoc0`, `set_itvco0`,
+    `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, `set_itv_infty_o`,
+    `set_itv_infty_c`, `set_itv_pinfty_bnd`, `set_itv_bnd_ninfty`, `setUitv1`,
+    `setU1itv`, `set_itvI`, `neitvE`, `neitvP`, `setitv0`, `has_lbound_itv`,
+    `has_ubound_itv`, `hasNlbound`, `hasNubound`, `opp_itv_bnd_infty`,
+    `opp_itv_infty_bnd`, `opp_itv_bnd_bnd`, `opp_itvoo`,
+    `setCitvl`, `setCitvr`, `set_itv_splitI`, `setCitv`, `set_itv_splitD`,
+    `mem_1B_itvcc`, `conv_id`, `convEl`, `convEr`, `conv10`, `conv0`,
+    `conv1`, `conv_sym`, `conv_flat`, `leW_conv`, `leW_factor`,
+    `factor_flat`, `factorl`, `ndconvE`, `factorr`, `factorK`,
+    `convK`, `conv_inj`, `factor_inj`, `conv_bij`, `factor_bij`,
+    `le_conv`, `le_factor`, `lt_conv`, `lt_factor`, `conv_itv_bij`,
+    `factor_itv_bij`, `mem_conv_itv`, `mem_conv_itvcc`, `range_conv`,
+    `range_factor`, `mem_factor_itv`,
+    `set_itv_ge`, `trivIset_set_itv_nth`, `disjoint_itvxx`, `lt_disjoint`,
+    `disjoint_neitv`, `neitv_bnd1`, `neitv_bnd2` (from `set_interval.v`)
+  + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`,
+    `has_lb_ubN`, `has_ubPn`, `has_lbPn` (from `reals.v`)
+- in `classical_sets.v`:
+  + lemma `bigsetU_sup`
+- in `lebesgue_integral.v`:
+  + lemmas `emeasurable_fun_fsum`, `ge0_integral_fsum`
+- in `ereal.v`:
+  + lemma `fsumEFin`
+- in `lebesgue_measure.v`:
+  + definition `ErealGenInftyO.R` and lemma `ErealGenInftyO.measurableE`
+  + lemma `sub1set`
+- in `constructive_ereal.v`:
+  + lemmas `lteN10`, `leeN10`
+  + lemmas `le0_fin_numE`
+  + lemmas `fine_lt0`, `fine_le0`
+- in `sequences.v`:
+  + lemmas `is_cvg_ereal_npos_natsum_cond`, `lee_npeseries`,
+    `is_cvg_npeseries_cond`, `is_cvg_npeseries`, `npeseries_le0`,
+    `is_cvg_ereal_npos_natsum`
+  + lemma `nnseries_is_cvg`
+- in `constructive_ereal.v`:
+  + lemma `fine_lt0E`
+- in file `normedtype.v`
+  + lemmas `closed_ballR_compact` and `locally_compactR`
+
+- in `sequences.v`:
+  + lemma `invr_cvg0` and `invr_cvg_pinfty`
+  + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`,
+    `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
+- in `classical_sets.v`:
+  + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
+- 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`
+
+- in `fsbig.v`:
+  + lemma `fsbig_setU_set1`
+- in `tooplogy.v`:
+  + lemmas `closed_bigsetU`, `accessible_finite_set_closed`
+
+
+- in file `classical_sets.v`,
+  + new lemmas `eq_image_id`, `subKimage`, `subimageK`, and `eq_imageK`.
+- in file `functions.v`,
+  + new lemmas `inv_oppr`, `preimageEoinv`, `preimageEinv`, and
+    `inv_funK`.
+- in file `mathcomp_extra.v`,
+  + new definition `inv_fun`.
+  + new lemmas `ler_ltP`, and `real_ltr_distlC`.
+- in file `constructive_ereal.v`,
+  + new lemmas `real_ltey`, `real_ltNye`, `real_leey`, `real_leNye`,
+    `fin_real`, `addNye`, `addeNy`, `gt0_muley`, `lt0_muley`, `gt0_muleNy`, and
+    `lt0_muleNy`.
+  + new lemmas `daddNye`, and `daddeNy`.
+- in file `ereal.v`,
+  + new lemmas `ereal_nbhs_pinfty_gt`, `ereal_nbhs_ninfty_lt`,
+    `ereal_nbhs_pinfty_real`, and `ereal_nbhs_ninfty_real`.
+- in file `normedtype.v`,
+  + new lemmas `nbhsNimage`, `nbhs_pinfty_real`, `nbhs_ninfty_real`,
+    `pinfty_ex_ge`, `cvgryPger`, `cvgryPgtr`, `cvgrNyPler`, `cvgrNyPltr`,
+    `cvgry_ger`, `cvgry_gtr`, `cvgrNy_ler`, `cvgrNy_ltr`, `cvgNry`, `cvgNrNy`,
+    `cvgry_ge`, `cvgry_gt`, `cvgrNy_le`, `cvgrNy_lt`, `cvgeyPger`, `cvgeyPgtr`,
+    `cvgeyPgty`, `cvgeyPgey`, `cvgeNyPler`, `cvgeNyPltr`, `cvgeNyPltNy`,
+    `cvgeNyPleNy`, `cvgey_ger`, `cvgey_gtr`, `cvgeNy_ler`, `cvgeNy_ltr`,
+    `cvgNey`, `cvgNeNy`, `cvgerNyP`, `cvgeyPge`, `cvgeyPgt`, `cvgeNyPle`,
+    `cvgeNyPlt`, `cvgey_ge`, `cvgey_gt`, `cvgeNy_le`, `cvgeNy_lt`, `cvgenyP`,
+    `normfZV`, `fcvgrPdist_lt`, `cvgrPdist_lt`, `cvgrPdistC_lt`,
+    `cvgr_dist_lt`, `cvgr_distC_lt`, `cvgr_dist_le`, `cvgr_distC_le`,
+    `nbhs_norm0P`, `cvgr0Pnorm_lt`, `cvgr0_norm_lt`, `cvgr0_norm_le`, `nbhsDl`,
+    `nbhsDr`, `nbhs0P`, `nbhs_right0P`, `nbhs_left0P`, `nbhs_right_gt`,
+    `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, `nbhs_right_ge`,
+    `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_le`, `nbhs_left_gt`,
+    `nbhs_left_ge`, `nbhsr0P`, `cvgrPdist_le`, `cvgrPdist_ltp`,
+    `cvgrPdist_lep`, `cvgrPdistC_le`, `cvgrPdistC_ltp`, `cvgrPdistC_lep`,
+    `cvgr0Pnorm_le`, `cvgr0Pnorm_ltp`, `cvgr0Pnorm_lep`, `cvgr_norm_lt`,
+    `cvgr_norm_le`, `cvgr_norm_gt`, `cvgr_norm_ge`, `cvgr_neq0`,
+    `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_gt`, `real_cvgr_ge`, `cvgr_lt`,
+    `cvgr_gt`, `cvgr_norm_lty`, `cvgr_norm_ley`, `cvgr_norm_gtNy`,
+    `cvgr_norm_geNy`, `fcvgr_dist_lt2P`, `cvgr_dist_lt2P`, `cvgr_dist_lt2`,
+    `cvgNP`, `norm_cvg0P`, `cvgVP`, `is_cvgVE`, `cvgr_to_ge`, `cvgr_to_le`,
+    `nbhs_EFin`, `nbhs_ereal_pinfty`, `nbhs_ereal_ninfty`, `fine_fcvg`,
+    `fcvg_is_fine`, `fine_cvg`, `cvg_is_fine`, `cvg_EFin`, `neq0_fine_cvgP`,
+    `cvgeNP`, `is_cvgeNE`, `cvge_to_ge`, `cvge_to_le`, `is_cvgeM`, `limeM`,
+    `cvge_ge`, `cvge_le`, `lim_nnesum`, `ltr0_cvgV0`, `cvgrVNy`, `ler_cvg_to`,
+    `gee_cvgy`, `lee_cvgNy`, `squeeze_fin`, and `lee_cvg_to`.
+- in file `sequences.v`,
+  + new lemma `nneseries_pinfty`.
+- in file `topology.v`,
+  + new lemmas `eq_cvg`, `eq_is_cvg`, `eq_near`, `cvg_toP`, `cvgNpoint`,
+    `filter_imply`, `nbhs_filter`, `near_fun`, `cvgnyPgt`, `cvgnyPgty`,
+    `cvgnyPgey`, `fcvg_ballP`, `fcvg_ball`, and `fcvg_ball2P`.
+- in `topology.v`, added `near do` and `near=> x do` tactic notations
+  to perform some tactics under a `\forall x \near F, ...` quantification.
+- in `normedtype.v`, added notations `^'+`, `^'-`, `+oo_R`, `-oo_R`
 
 - in file `topology.v`,
   + new definitions `quotient_topology`, and `quotient_open`.
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index e647c855cb..42f7c9f835 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1279,6 +1279,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 dbb1a589c1..37329347d9 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3673,12 +3673,6 @@ by move=> ->; have := projT2 (sigW (npts N)).
 Qed.
 
 End perfect_sets.
-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 *)
 
@@ -6795,6 +6789,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}.
@@ -6831,10 +6837,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 : 
@@ -6879,9 +6883,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 534fe0818cc26710ec81522a307c6f592f86fa8f Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 15:10:13 -0400
Subject: [PATCH 06/16] 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 c6a96b377b..9b710d394c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -136,6 +136,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 37329347d9..26b0ba248d 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -116,6 +116,13 @@ Require Import 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         *)
@@ -6789,9 +6796,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
@@ -6809,78 +6816,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.
@@ -6892,10 +6892,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 8607827305a9d4313f8722e40c9e3bb40481201d Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 10 Oct 2022 17:24:21 -0400
Subject: [PATCH 07/16] 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 26b0ba248d..62cbca15bc 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6856,7 +6856,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) //.
@@ -6877,9 +6877,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 a6ff41ae66bc6b1f0f01f458b6c1068bdc561e21 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 26 Oct 2022 10:35:21 +0900
Subject: [PATCH 08/16] typos

---
 theories/topology.v | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 62cbca15bc..3e408b36e9 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -117,12 +117,12 @@ Require Import 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         *)
@@ -3344,7 +3344,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.
 
@@ -6797,21 +6797,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).
@@ -6831,7 +6830,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.
@@ -6851,7 +6850,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.
@@ -6865,21 +6864,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 de839b1a05d87660fe3c96fde15ac897da7cebb6 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Tue, 22 Nov 2022 18:28:13 -0500
Subject: [PATCH 09/16] adding local notations for proof legibility

---
 theories/topology.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/topology.v b/theories/topology.v
index 3e408b36e9..d9d0c1efe6 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6817,8 +6817,14 @@ 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_.
 
+Local Notation sup_open := (@open weakT).
+Local Notation "'weak_open' i" := 
+  (@open (weak_topologicalType (f_ i))) (at level 0).
+Local Notation natural_open := (@open T).
+
 Lemma weak_sep_cvg (F : set (set T)) (x : T) :
   Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)).
 Proof.
@@ -6864,6 +6870,8 @@ apply: open_comp => // + _; rewrite /cvg_to => x U.
 by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf.
 Qed.
 
+Local Notation prod_open := (@open (subspace_topologicalType (range join_product))).
+
 Lemma join_product_open (A : set T) : open A ->
   open ((join_product @` A) : set (subspace (range join_product))).
 Proof.

From 94e8ce1eb207f4eee32f43406a46297d6f0b21fd Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 2 Jan 2023 12:10:11 -0500
Subject: [PATCH 10/16] merging product stuff

---
 theories/topology.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index d9d0c1efe6..56dd84ab4d 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6864,30 +6864,30 @@ 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 ? E].
-rewrite -E (_ : @^~ i = prod_topo_apply i) //.
-have -> : join_product @^-1` (prod_topo_apply i @^-1` B) = f_ i @^-1` B by [].
+rewrite -E (_ : @^~ i =  proj i) //.
+have -> : join_product @^-1` (proj i @^-1` B) = f_ i @^-1` B by [].
 apply: open_comp => // + _; rewrite /cvg_to => x U.
 by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf.
 Qed.
 
-Local Notation prod_open := (@open (subspace_topologicalType (range join_product))).
+Local Notation prod_open := 
+  (@open (subspace_topologicalType (range join_product))).
 
 Lemma join_product_open (A : set T) : open A ->
   open ((join_product @` A) : set (subspace (range join_product))).
 Proof.
 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)).
+pose B : set PU := proj i @^-1` (~` closure (f_ i @` ~` A)).
 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 [].
+  have -> : proj 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.
-exact/closed_openC/closed_closure.
+apply: open_subspaceW; apply: open_comp; last exact/closed_openC/closed_closure.
+by move=> + _; exact: proj_continuous.
 Qed.
 
 Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product.

From 8d830991168ecd92144f1221693f38c94e9e6376 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 2 Jan 2023 13:37:30 -0500
Subject: [PATCH 11/16] fixing changelog

---
 CHANGELOG_UNRELEASED.md | 51 +++++------------------------------------
 1 file changed, 6 insertions(+), 45 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9b710d394c..ae2bed6793 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -148,51 +148,7 @@
 
 
 - in file `classical_sets.v`,
-  + new lemmas `eq_image_id`, `subKimage`, `subimageK`, and `eq_imageK`.
-- in file `functions.v`,
-  + new lemmas `inv_oppr`, `preimageEoinv`, `preimageEinv`, and
-    `inv_funK`.
-- in file `mathcomp_extra.v`,
-  + new definition `inv_fun`.
-  + new lemmas `ler_ltP`, and `real_ltr_distlC`.
-- in file `constructive_ereal.v`,
-  + new lemmas `real_ltey`, `real_ltNye`, `real_leey`, `real_leNye`,
-    `fin_real`, `addNye`, `addeNy`, `gt0_muley`, `lt0_muley`, `gt0_muleNy`, and
-    `lt0_muleNy`.
-  + new lemmas `daddNye`, and `daddeNy`.
-- in file `ereal.v`,
-  + new lemmas `ereal_nbhs_pinfty_gt`, `ereal_nbhs_ninfty_lt`,
-    `ereal_nbhs_pinfty_real`, and `ereal_nbhs_ninfty_real`.
-- in file `normedtype.v`,
-  + new lemmas `nbhsNimage`, `nbhs_pinfty_real`, `nbhs_ninfty_real`,
-    `pinfty_ex_ge`, `cvgryPger`, `cvgryPgtr`, `cvgrNyPler`, `cvgrNyPltr`,
-    `cvgry_ger`, `cvgry_gtr`, `cvgrNy_ler`, `cvgrNy_ltr`, `cvgNry`, `cvgNrNy`,
-    `cvgry_ge`, `cvgry_gt`, `cvgrNy_le`, `cvgrNy_lt`, `cvgeyPger`, `cvgeyPgtr`,
-    `cvgeyPgty`, `cvgeyPgey`, `cvgeNyPler`, `cvgeNyPltr`, `cvgeNyPltNy`,
-    `cvgeNyPleNy`, `cvgey_ger`, `cvgey_gtr`, `cvgeNy_ler`, `cvgeNy_ltr`,
-    `cvgNey`, `cvgNeNy`, `cvgerNyP`, `cvgeyPge`, `cvgeyPgt`, `cvgeNyPle`,
-    `cvgeNyPlt`, `cvgey_ge`, `cvgey_gt`, `cvgeNy_le`, `cvgeNy_lt`, `cvgenyP`,
-    `normfZV`, `fcvgrPdist_lt`, `cvgrPdist_lt`, `cvgrPdistC_lt`,
-    `cvgr_dist_lt`, `cvgr_distC_lt`, `cvgr_dist_le`, `cvgr_distC_le`,
-    `nbhs_norm0P`, `cvgr0Pnorm_lt`, `cvgr0_norm_lt`, `cvgr0_norm_le`, `nbhsDl`,
-    `nbhsDr`, `nbhs0P`, `nbhs_right0P`, `nbhs_left0P`, `nbhs_right_gt`,
-    `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`, `nbhs_right_ge`,
-    `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_le`, `nbhs_left_gt`,
-    `nbhs_left_ge`, `nbhsr0P`, `cvgrPdist_le`, `cvgrPdist_ltp`,
-    `cvgrPdist_lep`, `cvgrPdistC_le`, `cvgrPdistC_ltp`, `cvgrPdistC_lep`,
-    `cvgr0Pnorm_le`, `cvgr0Pnorm_ltp`, `cvgr0Pnorm_lep`, `cvgr_norm_lt`,
-    `cvgr_norm_le`, `cvgr_norm_gt`, `cvgr_norm_ge`, `cvgr_neq0`,
-    `real_cvgr_lt`, `real_cvgr_le`, `real_cvgr_gt`, `real_cvgr_ge`, `cvgr_lt`,
-    `cvgr_gt`, `cvgr_norm_lty`, `cvgr_norm_ley`, `cvgr_norm_gtNy`,
-    `cvgr_norm_geNy`, `fcvgr_dist_lt2P`, `cvgr_dist_lt2P`, `cvgr_dist_lt2`,
-    `cvgNP`, `norm_cvg0P`, `cvgVP`, `is_cvgVE`, `cvgr_to_ge`, `cvgr_to_le`,
-    `nbhs_EFin`, `nbhs_ereal_pinfty`, `nbhs_ereal_ninfty`, `fine_fcvg`,
-    `fcvg_is_fine`, `fine_cvg`, `cvg_is_fine`, `cvg_EFin`, `neq0_fine_cvgP`,
-    `cvgeNP`, `is_cvgeNE`, `cvge_to_ge`, `cvge_to_le`, `is_cvgeM`, `limeM`,
-    `cvge_ge`, `cvge_le`, `lim_nnesum`, `ltr0_cvgV0`, `cvgrVNy`, `ler_cvg_to`,
-    `gee_cvgy`, `lee_cvgNy`, `squeeze_fin`, and `lee_cvg_to`.
-- in file `sequences.v`,
-  + new lemma `nneseries_pinfty`.
+  + new lemma `preimage_range`.
 - in file `topology.v`,
   + new lemmas `eq_cvg`, `eq_is_cvg`, `eq_near`, `cvg_toP`, `cvgNpoint`,
     `filter_imply`, `nbhs_filter`, `near_fun`, `cvgnyPgt`, `cvgnyPgty`,
@@ -206,6 +162,11 @@
   + new lemmas `pi_continuous`, `quotient_continuous`, and
     `repr_comp_continuous`.
 
+  + new definitions `hausdorff_accessible`, `separates_points_from_closed`, and 
+    `join_product`.
+  + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
+    `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
+    `join_product_weak`.
 ### Changed
 
 - in `fsbigop.v`:

From d5bc8566457a18357a4d5dea5ace4a7ee2a60ad4 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 6 Feb 2023 21:57:36 +0900
Subject: [PATCH 12/16] specialized conjunctions to use less brackets and
 splits

---
 CHANGELOG_UNRELEASED.md |   5 ++
 classical/boolp.v       |   8 +++
 theories/normedtype.v   |  12 ++--
 theories/sequences.v    |   3 +-
 theories/topology.v     | 134 ++++++++++++++++++++--------------------
 5 files changed, 86 insertions(+), 76 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ae2bed6793..f959910ce1 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -167,6 +167,9 @@
   + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
     `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
     `join_product_weak`.
+- in `boolp.v`:
+  + lemma `forallp_asboolPn2`
+
 ### Changed
 
 - in `fsbigop.v`:
@@ -184,6 +187,8 @@
   + canonical `fimfun_comRingType`
   + lemma `max_fimfun_subproof`
   + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}`
+- in `topology.v`:
+  + `Topological.ax2`
 
 ### Renamed
 
diff --git a/classical/boolp.v b/classical/boolp.v
index 7ff24a1c8a..7d2d0ba576 100644
--- a/classical/boolp.v
+++ b/classical/boolp.v
@@ -676,6 +676,14 @@ split=> [[x Px NQx] /(_ x Px)//|]; apply: contra_notP => + x Px.
 by apply: contra_notP => NQx; exists x.
 Qed.
 
+Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} :
+  reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[<exists2 x : T, P x & Q x>]).
+Proof.
+apply: (iffP idP)=> [/asboolPn NP x|NP].
+  by move/forallPNP : NP => /(_ x)/and_rec/not_andP.
+by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact.
+Qed.
+
 Module FunOrder.
 Section FunOrder.
 Import Order.TTheory.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index d2e2159cb6..d2f2474160 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -3940,26 +3940,26 @@ Qed.
 Lemma nbhs_open_ereal_lt r (f : R -> R) : r < f r ->
   nbhs r%:E [set y | y < (f r)%:E]%E.
 Proof.
-move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_lt_ereal | rewrite /= lte_fin].
 Qed.
 
 Lemma nbhs_open_ereal_gt r (f : R -> R) : f r < r ->
   nbhs r%:E [set y | (f r)%:E < y]%E.
 Proof.
-move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_gt_ereal | rewrite /= lte_fin].
 Qed.
 
 Lemma nbhs_open_ereal_pinfty r : (nbhs +oo [set y | r%:E < y])%E.
 Proof.
-rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_gt_ereal | rewrite /= ltry].
 Qed.
 
 Lemma nbhs_open_ereal_ninfty r : (nbhs -oo [set y | y < r%:E])%E.
 Proof.
-rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_lt_ereal | rewrite /= ltNyr].
 Qed.
 
@@ -4290,7 +4290,7 @@ move=> oU; have [->|U0] := eqVneq U set0.
 apply/seteqP; split=> [x Ux|x [p _ Ipx]]; last exact: bigcup_ointsub_sub Ipx.
 suff [q Iqx] : exists q, bigcup_ointsub U q x.
   by exists q => //=; rewrite in_setE; case: Iqx => A [[_ _ +] ? _]; exact.
-have : nbhs x U by rewrite nbhsE /=; exists U; split => //.
+have : nbhs x U by rewrite nbhsE /=; exists U.
 rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ => -[_/posnumP[r] xrU].
 have /rat_in_itvoo[q qxxr] : (x - r%:num < x + r%:num)%R.
   by rewrite ltr_subl_addr -addrA ltr_addl.
@@ -4804,7 +4804,7 @@ move=> C D FC f_D; have {}f_D :
   have exPj : forall j, exists Bj, open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
     move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj].
     by rewrite row_simpl'; exists Bj.
-  exists [set g | forall j, (get (Pj j)) (g j)]; split; last first.
+  exists [set g | forall j, (get (Pj j)) (g j)]; last first.
     move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'.
     by have /getPex [_ /(_ _ (Pg j))] := exPj j.
   split; last by move=> j; have /getPex [[]] := exPj j.
diff --git a/theories/sequences.v b/theories/sequences.v
index 568fbf6ad9..5ddf525490 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1282,8 +1282,7 @@ Lemma cvg_nseries_near (u : nat^nat) : cvg (nseries u) ->
   \forall n \near \oo, u n = 0%N.
 Proof.
 move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l].
-  exists [set l]; split; last by split.
-  by exists [set l] => //; rewrite bigcup_set1.
+  by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1.
 have /ul[b _ bul] : nbhs l [set l.-1; l].
   by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1.
 exists (maxn a b) => // n /= abn.
diff --git a/theories/topology.v b/theories/topology.v
index 56dd84ab4d..810217f4f5 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -1599,7 +1599,7 @@ Record mixin_of (T : Type) (nbhs : T -> set (set T)) := Mixin {
   open : set (set T) ;
   ax1 : forall p : T, ProperFilter (nbhs p) ;
   ax2 : forall p : T, nbhs p =
-    [set A : set T | exists B : set T, open B /\ B p /\ B `<=` A] ;
+    [set A : set T | exists B : set T, [/\ open B, B p & B `<=` A] ] ;
   ax3 : open = [set A : set T | A `<=` nbhs^~ A ]
 }.
 
@@ -1678,17 +1678,17 @@ Proof. exact: (@nbhs_pfilter). Qed.
 Canonical nbhs_filter_on (x : T) := FilterType (nbhs x) (@nbhs_filter x).
 
 Lemma nbhsE (p : T) :
-  nbhs p = [set A : set T | exists B : set T, open_nbhs p B /\ B `<=` A].
+  nbhs p = [set A : set T | exists2 B : set T, open_nbhs p B & B `<=` A].
 Proof.
-have -> : nbhs p = [set A : set T | exists B, open B /\ B p /\ B `<=` A].
+have -> : nbhs p = [set A : set T | exists B, [/\ open B, B p & B `<=` A] ].
   exact: Topological.ax2.
-by rewrite predeqE => A; split=> [[B [? []]]|[B [[]]]]; exists B.
+by rewrite predeqE => A; split=> [[B [?]]|[B[]]]; exists B.
 Qed.
 
 Lemma open_nbhsE (p : T) (A : set T) : open_nbhs p A = (open A /\ nbhs p A).
 Proof.
-rewrite nbhsE propeqE; split=> [[? ?]|[? [B [[? ?] BA]]]]; split => //;
-  [by exists A; split | exact: BA].
+by rewrite nbhsE propeqE; split=> [[? ?]|[? [B [? ?] BA]]]; split => //;
+  [exists A | exact: BA].
 Qed.
 
 Definition interior (A : set T) := (@nbhs _ T)^~ A.
@@ -1697,19 +1697,19 @@ Local Notation "A ^°" := (interior A).
 
 Lemma interior_subset (A : set T) : A^° `<=` A.
 Proof.
-by move=> p; rewrite /interior nbhsE => -[? [[??]]]; apply.
+by move=> p; rewrite /interior nbhsE => -[? [? ?]]; apply.
 Qed.
 
 Lemma openE : open = [set A : set T | A `<=` A^°].
 Proof. exact: Topological.ax3. Qed.
 
 Lemma nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
-Proof. by rewrite nbhsE => - [? [[_ ?]]]; apply. Qed.
+Proof. by rewrite nbhsE => - [? [_ ?]]; apply. Qed.
 
 Lemma nbhs_interior (p : T) (A : set T) : nbhs p A -> nbhs p A^°.
 Proof.
-rewrite nbhsE /open_nbhs openE => - [B [[Bop Bp] sBA]].
-by exists B; split=> // q Bq; apply: filterS sBA _; apply: Bop.
+rewrite nbhsE /open_nbhs openE => - [B [Bop Bp] sBA].
+by exists B => // q Bq; apply: filterS sBA _; apply: Bop.
 Qed.
 
 Lemma open0 : open set0.
@@ -1745,15 +1745,15 @@ Qed.
 
 Lemma open_interior (A : set T) : open A^°.
 Proof.
-rewrite openE => p; rewrite /interior nbhsE => - [B [[Bop Bp]]].
+rewrite openE => p; rewrite /interior nbhsE => - [B [Bop Bp]].
 by rewrite open_subsetE //; exists B.
 Qed.
 
 Lemma interior_bigcup I (D : set I) (f : I -> set T) :
   \bigcup_(i in D) (f i)^° `<=` (\bigcup_(i in D) f i)^°.
 Proof.
-move=> p [i Di]; rewrite /interior nbhsE => - [B [[Bop Bp] sBfi]].
-by exists B; split=> // ? /sBfi; exists i.
+move=> p [i Di]; rewrite /interior nbhsE => - [B [Bop Bp] sBfi].
+by exists B => // ? /sBfi; exists i.
 Qed.
 
 Lemma open_nbhsT (p : T) : open_nbhs p setT.
@@ -1764,14 +1764,14 @@ Lemma open_nbhsI (p : T) (A B : set T) :
 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.
+Proof. by rewrite nbhsE => p_A; exists A. Qed.
 
 Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°.
 Proof.
-rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 [?]] | []].
+rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []].
 - by rewrite subsetI => // -[? ?]; split; exists B0.
-- move=> -[B0 [? ?]] [B1 [? ?]]; exists (B0 `&` B1); split;
-  [exact: open_nbhsI | by rewrite subsetI; split; apply: subIset; [left|right]].
+- by move=> -[B0 ? ?] [B1 ? ?]; exists (B0 `&` B1);
+  [exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]].
 Qed.
 
 End Topological1.
@@ -1795,8 +1795,8 @@ Lemma continuousP (S T : topologicalType) (f : S -> T) :
   continuous f <-> forall A, open A -> open (f @^-1` A).
 Proof.
 split=> fcont; first by rewrite !openE => A Aop ? /Aop /fcont.
-move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [[Bop Bfs] sBA]].
-by exists (f @^-1` B); split; [split=> //; apply/fcont|move=> ? /sBA].
+move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA].
+by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA].
 Qed.
 
 Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x :
@@ -1922,10 +1922,9 @@ Local Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).
 Lemma within_interior (x : T) : A^° x -> within A (nbhs x) = nbhs x.
 Proof.
 move=> Aox; rewrite eqEsubset; split; last exact: cvg_within.
-rewrite ?nbhsE => W /= => [[B [+ BsubW]]].
+rewrite ?nbhsE => W /= => [[B + BsubW]].
 rewrite open_nbhsE => [[oB nbhsB]].
-exists (B `&` A^°); split; last first.
-  by move=> t /= [] /BsubW + /interior_subset; apply.
+exists (B `&` A^°); last by move=> t /= [] /BsubW + /interior_subset; apply.
 rewrite open_nbhsE; split; first by apply: openI => //; exact: open_interior.
 by apply: filterI => //; move:(open_interior A); rewrite openE; exact.
 Qed.
@@ -1972,9 +1971,9 @@ Program Definition topologyOfFilterMixin : Topological.mixin_of nbhs' :=
   @Topological.Mixin T nbhs' open_of_nbhs _ _ _.
 Next Obligation.
 move=> p; rewrite predeqE => A; split=> [p_A|]; last first.
-  by move=> [B [Bop [Bp sBA]]]; apply: filterS sBA _; apply: Bop.
-exists (nbhs'^~ A); split; first by move=> ?; apply: nbhs'_nbhs'.
-by split => // q /nbhs'_singleton.
+  by move=> [B [Bop Bp sBA]]; apply: filterS sBA _; apply: Bop.
+exists (nbhs'^~ A) ; split => //; first by move=> ?; apply: nbhs'_nbhs'.
+by move=> q /nbhs'_singleton.
 Qed.
 Next Obligation. done. Qed.
 
@@ -1991,19 +1990,19 @@ Hypothesis (op_bigU : forall (I : Type) (f : I -> set T),
   (forall i, op (f i)) -> op (\bigcup_i f i)).
 
 Definition nbhs_of_open (p : T) (A : set T) :=
-  exists B, op B /\ B p /\ B `<=` A.
+  exists B, [/\ op B, B p & B `<=` A].
 
 Program Definition topologyOfOpenMixin : Topological.mixin_of nbhs_of_open :=
   @Topological.Mixin T nbhs_of_open op _ _ _.
 Next Obligation.
 move=> p; apply: Build_ProperFilter.
-  by move=> A [B [_ [Bp sBA]]]; exists p; apply: sBA.
+  by move=> A [B [_ Bp sBA]]; exists p; apply: sBA.
 split; first by exists setT.
-  move=> A B [C [Cop [Cp sCA]]] [D [Dop [Dp sDB]]].
-  exists (C `&` D); split; first exact: opI.
-  by split=> // q [/sCA Aq /sDB Bq].
-move=> A B sAB [C [Cop [p_C sCA]]].
-by exists C; split=> //; split=> //; apply: subset_trans sAB.
+  move=> A B [C [Cop Cp sCA]] [D [Dop Dp sDB]].
+  exists (C `&` D); split => //; first exact: opI.
+  by move=> q [/sCA Aq /sDB Bq].
+move=> A B sAB [C [Cop p_C sCA]].
+by exists C; split=> //; apply: subset_trans sAB.
 Qed.
 Next Obligation. done. Qed.
 Next Obligation.
@@ -2012,7 +2011,7 @@ rewrite predeqE => A; split=> [Aop p Ap|Aop].
 suff -> : A = \bigcup_(B : {B : set T & op B /\ B `<=` A}) projT1 B.
   by apply: op_bigU => B; have [] := projT2 B.
 rewrite predeqE => p; split=> [|[B _ Bp]]; last by have [_] := projT2 B; apply.
-by move=> /Aop [B [Bop [Bp sBA]]]; exists (existT _ B (conj Bop sBA)).
+by move=> /Aop [B [Bop Bp sBA]]; exists (existT _ B (conj Bop sBA)).
 Qed.
 
 End TopologyOfOpen.
@@ -2355,12 +2354,12 @@ Lemma cvg_image (F : set (set S)) (s : S) :
   F --> (s : weak_topologicalType) <-> [set f @` A | A in F] --> f s.
 Proof.
 move=> FF fsurj; split=> [cvFs|cvfFfs].
-  move=> A /weak_continuous [B [Bop [Bs sBAf]]].
+  move=> A /weak_continuous [B [Bop Bs sBAf]].
   have /cvFs FB : nbhs (s : weak_topologicalType) 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]]].
-have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B; split.
+move=> A /= [_ [[B Bop <-] Bfs sBfA]].
+have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B.
 rewrite nbhs_filterE; apply: filterS FC.
 by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image.
 Qed.
@@ -2387,16 +2386,16 @@ Lemma cvg_sup (F : set (set T)) (t : T) :
   Filter F -> F --> (t : sup_topologicalType) <-> forall i, F --> (t : TS i).
 Proof.
 move=> Ffilt; split=> cvFt.
-  move=> i A /=; rewrite (@nbhsE (TS i)) => - [B [[Bop Bt] sBA]].
+  move=> i A /=; rewrite (@nbhsE (TS 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=> [_ [[[B sB <-] [C BC Ct]] sUBA]].
+move=> [_ [[B sB <-] [C BC Ct] sUBA]].
 rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C).
-  by move=> ??; exists C.
+  by move=> ? ?; exists C.
 have /sB [D sD IDeC] := BC; rewrite -IDeC; apply: filter_bigI => E DE.
 have /sD := DE; rewrite inE => - [i _]; rewrite openE => Eop.
 by apply: (cvFt i); apply: Eop; move: Ct; rewrite -IDeC => /(_ _ DE).
@@ -2426,10 +2425,10 @@ Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x.
 Proof.
 rewrite predeqE => A; split=> [x_A|[x_A Ax]].
   split; last exact: nbhs_singleton.
-  move: x_A; rewrite nbhsE => -[B [x_B sBA]]; rewrite /dnbhs nbhsE.
-  by exists B; split=> // ? /sBA.
-move: x_A; rewrite /dnbhs !nbhsE => -[B [x_B sBA]]; exists B.
-by split=> // y /sBA Ay; case: (eqVneq y x) => [->|].
+  move: x_A; rewrite nbhsE => -[B [oB x_B sBA]]; rewrite /dnbhs nbhsE.
+  by exists B => // ? /sBA.
+move: x_A; rewrite /dnbhs !nbhsE => -[B [oB x_B sBA]]; exists B => //.
+by move=> y /sBA Ay; case: (eqVneq y x) => [->|].
 Qed.
 
 Global Instance dnbhs_filter {T : topologicalType} (x : T) : Filter x^'.
@@ -2460,7 +2459,7 @@ Lemma meets_openr {T : topologicalType} (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.
+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) :
@@ -2571,11 +2570,11 @@ Proof.
 rewrite predeqE => A; split=> Acl p; last first.
   by move=> clAp; apply: Acl; rewrite -nbhs_nearE => /clAp [? []].
 rewrite -nbhs_nearE nbhsE => /asboolP.
-rewrite asbool_neg => /forallp_asboolPn clAp.
-apply: Acl => B; rewrite nbhsE => - [C [p_C sCB]].
+rewrite asbool_neg => /forallp_asboolPn2 clAp.
+apply: Acl => B; rewrite nbhsE => - [C [oC pC]].
 have /asboolP := clAp C.
-rewrite asbool_neg asbool_and => /nandP [/asboolP//|/existsp_asboolPn [q]].
-move/asboolP; rewrite asbool_neg => /imply_asboolPn [/sCB Bq /contrapT Aq].
+rewrite asbool_or 2!asbool_neg => /orP[/asboolP/not_andP[]//|/existsp_asboolPn [q]].
+move/asboolP; rewrite asbool_neg => /imply_asboolPn[+ /contrapT Aq sCB] => /sCB.
 by exists q.
 Qed.
 
@@ -2604,7 +2603,7 @@ Proof.
 rewrite !closedE=> f_continuous D_cl x /= xDf.
 apply: D_cl; apply: contra_not xDf => fxD.
 have NDfx : ~ D (f x).
-  by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [[??]]]; apply.
+  by move: fxD; rewrite -nbhs_nearE nbhsE => - [A [? ?]]; apply.
 by apply: f_continuous fxD; rewrite inE.
 Qed.
 
@@ -3061,7 +3060,7 @@ Qed.
 
 Lemma dfwith_continuous g (i : I) : continuous (dfwith g _ : K i -> PK).
 Proof.
-move=> z U [] P [] [] Q QfinP <- [] [] V JV Vpz.
+move=> z U [] P [] [] Q QfinP <- [] V JV Vpz.
 move/(@preimage_subset _ _ (dfwith g i))/filterS; apply.
 apply: (@filterS _ _ _ ((dfwith g i) @^-1` V)); first by exists V.
 have [L Lsub /[dup] VL <-] := QfinP _ JV; rewrite preimage_bigcap.
@@ -3249,14 +3248,14 @@ Lemma accessible_closed_set1 : accessible_space -> forall x, closed [set x].
 Proof.
 move=> T1 x; rewrite -[X in closed X]setCK; apply: open_closedC.
 rewrite openE => y /eqP /T1 [U [oU [yU xU]]].
-rewrite /interior nbhsE /=; exists U; split; last by rewrite subsetC1.
-by split=> //; rewrite inE in yU.
+rewrite /interior nbhsE /=; exists U; last by rewrite subsetC1.
+by split=> //; exact: set_mem.
 Qed.
 
 Lemma accessible_kolmogorov : accessible_space -> kolmogorov_space.
 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.
+by rewrite nbhsE inE; exists A => //; rewrite inE in xA.
 Qed.
 
 Lemma accessible_finite_set_closed :
@@ -3333,7 +3332,7 @@ rewrite propeqE; split => [T_filterT2|T_openT2] x y.
   rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].
   move=> /asboolPn; rewrite -set0P => /negP; rewrite negbK => /eqP AIB_eq0.
   move: xA yB; rewrite !nbhsE.
-  move=> - [oA [[oA_open oAx] oAA]] [oB [[oB_open oBx] oBB]].
+  move=> - [oA [oA_open oAx] oAA] [oB [oB_open oBx] oBB].
   by exists (oA, oB); rewrite ?inE; split => //; apply: subsetI_eq0 AIB_eq0.
 apply: contraPP => /eqP /T_openT2[[/=A B]].
 rewrite !inE => - [xA yB] [Aopen Bopen /eqP AIB_eq0].
@@ -4257,12 +4256,12 @@ Qed.
 Lemma weak_ent_nbhs : nbhs = nbhs_ weak_ent.
 Proof.
 rewrite predeq2E => x V; split.
-  case=> [? [[B  ? <-] [? BsubV]]]; have: nbhs (f x) B by apply: open_nbhs_nbhs.
+  case=> [? [[B  ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs.
   move=> /nbhsP [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W.
   by move=>??; exact/BsubV/WsubB.
 case=> W [V' entV' V'subW] /filterS; apply.
 have : nbhs (f x) to_set V' (f x) by apply/nbhsP; exists V'.
-rewrite (@nbhsE U) => [[O [[openU Ofx Osub]]]].
+rewrite (@nbhsE U) => [[O [openU Ofx Osub]]].
 (exists (f @^-1` O); repeat split => //); first by exists O => //.
 by move=> w ? ; apply: V'subW; exact: Osub.
 Qed.
@@ -4338,7 +4337,7 @@ Qed.
 Lemma sup_ent_nbhs : @nbhs Tt Tt = nbhs_ sup_ent.
 Proof.
 rewrite predeq2E => x V; split.
-  rewrite /nbhs_of_open => [[? [[B  + <-] [[W BW Wx] BV]]]] => /(_ W BW) [].
+  rewrite /nbhs_of_open => [[? [[B  + <-] [W BW Wx] BV]]] => /(_ W BW) [].
   move=> F Fsup Weq; move: Weq Wx BW => <- Fx BF.
   case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
     suff -> : V = setT  by exists setT; apply: filterT; exact: sup_ent_filter.
@@ -5621,7 +5620,7 @@ Lemma uniform_nbhs (f : fct_RestrictedUniformTopology) P:
   nbhs f P <-> (exists E, entourage E /\
     [set h | forall y, A y -> E(f y, h y)] `<=` P).
 Proof.
-split=> [[Q [[/= W oW <- /=] [Wf subP]]]|[E [entE subP]]].
+split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]].
   rewrite openE /= /interior in oW.
   case: (oW _ Wf) => ? [ /= E entE] Esub subW.
   exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]].
@@ -6410,7 +6409,7 @@ Section SubspaceOpen.
 Lemma open_subspace1out (x : subspace A) : ~ A x -> open [set x].
 Proof.
 move=> /nbhs_subspace_out E; have : nbhs x [set x] by rewrite /nbhs //= -E.
-rewrite nbhsE => [[U [[]]]] oU Ux Usub; suff : U = [set x] by move=> <-.
+rewrite nbhsE => [[U []]] oU Ux Usub; suff : U = [set x] by move=> <-.
 by rewrite eqEsubset; split => // t ->.
 Qed.
 
@@ -6821,7 +6820,7 @@ Let weakT := @sup_topologicalType T I
 Let PU := product_topologicalType U_.
 
 Local Notation sup_open := (@open weakT).
-Local Notation "'weak_open' i" := 
+Local Notation "'weak_open' i" :=
   (@open (weak_topologicalType (f_ i))) (at level 0).
 Local Notation natural_open := (@open T).
 
@@ -6831,12 +6830,12 @@ Proof.
 move=> FF; split.
   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 ?]]]].
+  case=> B [[C oC <- ?]] /filterS; apply; apply: FTx; rewrite /= nbhsE.
+  by exists (f_ i @^-1` C) => //; 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])); split; [split=>//|].
+exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [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.
@@ -6870,7 +6869,7 @@ apply: open_comp => // + _; rewrite /cvg_to => x U.
 by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf.
 Qed.
 
-Local Notation prod_open := 
+Local Notation prod_open :=
   (@open (subspace_topologicalType (range join_product))).
 
 Lemma join_product_open (A : set T) : open A ->
@@ -7010,9 +7009,8 @@ split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact.
 move=> + x => /(_ x)/near_powerset_filter_fromP.
 case; first by move=> ? ?; exact: continuous_subspaceW.
 move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U.
-  move: nbhsU; rewrite nbhsE => -[] W [[oW Wx WU]] /(_ W).
-  move/(_ (continuous_subspaceW WU wctsf)); apply => //.
-  by exists W; split.
+  move: nbhsU; rewrite nbhsE => -[] W [oW Wx WU] /(_ W).
+  by move/(_ (continuous_subspaceW WU wctsf)); apply => //; exists W.
 move/nbhs_singleton: nbhsU; move: x; apply/in_setP.
 by rewrite -continuous_open_subspace.
 Unshelve. end_near. Qed.

From e81e9adcc84a35565e268ee824b0c85aa702c80d Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 6 Feb 2023 10:03:16 -0500
Subject: [PATCH 13/16] fixing grammar

---
 theories/topology.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 810217f4f5..791ec0c5da 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -116,7 +116,7 @@ Require Import 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 *)
+(*    separate_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.       *)
@@ -6795,13 +6795,13 @@ Qed.
 
 End SubspaceWeak.
 
-Definition separates_points_from_closed {I : Type} {T : topologicalType}
+Definition separate_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 embedding a space T into a product. The key interface
-   is 'separates_points_from_closed', which guarantees that the topologies
+   is 'separate_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
@@ -6811,7 +6811,7 @@ Section product_embeddings.
 Context {I : choiceType} {T : topologicalType} {U_ : I -> topologicalType}.
 Variable (f_ : forall i, T -> U_ i).
 
-Hypothesis sepf : separates_points_from_closed f_.
+Hypothesis sepf : separate_points_from_closed f_.
 Hypothesis ctsf : forall i, continuous (f_ i).
 
 Let weakT := @sup_topologicalType T I

From f38da333f4afbe0489a1d1431eed748b18512600 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 6 Feb 2023 11:16:46 -0500
Subject: [PATCH 14/16] fix changelog

---
 CHANGELOG_UNRELEASED.md | 106 +++-------------------------------------
 1 file changed, 7 insertions(+), 99 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f959910ce1..60b4b08995 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -63,112 +63,22 @@
 - in `constructive_ereal.v`:
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`
   + lemma `fin_num_sume_distrr`
-  + lemmas `set_compose_subset`, `compose_diag`
-  + notation `\;` for the composition of relations
-- OPAM package `coq-mathcomp-classical` containing `boolp.v`
-- file `all_classical.v`
-- in file `mathcomp_extra.v`:
-  + lemmas `pred_oappE` and `pred_oapp_set` (from `classical_sets.v`)
-  + lemma `sumr_le0`
-- in file `fsbigop.v`:
-  + lemmas `fsumr_ge0`, `fsumr_le0`, `fsumr_gt0`, `fsumr_lt0`, `pfsumr_eq0`,
-    `pair_fsbig`, `exchange_fsbig`
-- in file `ereal.v`:
-  + notation `\sum_(_ \in _) _` (from `fsbigop.v`)
-  + lemmas `fsume_ge0`, `fsume_le0`, `fsume_gt0`, `fsume_lt0`,
-    `pfsume_eq0`, `lee_fsum_nneg_subset`, `lee_fsum`,
-    `ge0_mule_fsumr`, `ge0_mule_fsuml` (from `fsbigop.v`)
-  + lemmas `finite_supportNe`, `dual_fsumeE`, `dfsume_ge0`, `dfsume_le0`,
-    `dfsume_gt0`, `dfsume_lt0`, `pdfsume_eq0`, `le0_mule_dfsumr`, `le0_mule_dfsuml`
-- file `classical/set_interval.v`
-- in file `classical/set_interval.v`:
-  + definitions `neitv`, `set_itv_infty_set0`, `set_itvE`,
-    `disjoint_itv`, `conv`, `factor`, `ndconv` (from `set_interval.v`)
-  + lemmas `neitv_lt_bnd`, `set_itvP`, `subset_itvP`, `set_itvoo`, `set_itv_cc`,
-    `set_itvco`, `set_itvoc`, `set_itv1`, `set_itvoo0`, `set_itvoc0`, `set_itvco0`,
-    `set_itv_infty_infty`, `set_itv_o_infty`, `set_itv_c_infty`, `set_itv_infty_o`,
-    `set_itv_infty_c`, `set_itv_pinfty_bnd`, `set_itv_bnd_ninfty`, `setUitv1`,
-    `setU1itv`, `set_itvI`, `neitvE`, `neitvP`, `setitv0`, `has_lbound_itv`,
-    `has_ubound_itv`, `hasNlbound`, `hasNubound`, `opp_itv_bnd_infty`,
-    `opp_itv_infty_bnd`, `opp_itv_bnd_bnd`, `opp_itvoo`,
-    `setCitvl`, `setCitvr`, `set_itv_splitI`, `setCitv`, `set_itv_splitD`,
-    `mem_1B_itvcc`, `conv_id`, `convEl`, `convEr`, `conv10`, `conv0`,
-    `conv1`, `conv_sym`, `conv_flat`, `leW_conv`, `leW_factor`,
-    `factor_flat`, `factorl`, `ndconvE`, `factorr`, `factorK`,
-    `convK`, `conv_inj`, `factor_inj`, `conv_bij`, `factor_bij`,
-    `le_conv`, `le_factor`, `lt_conv`, `lt_factor`, `conv_itv_bij`,
-    `factor_itv_bij`, `mem_conv_itv`, `mem_conv_itvcc`, `range_conv`,
-    `range_factor`, `mem_factor_itv`,
-    `set_itv_ge`, `trivIset_set_itv_nth`, `disjoint_itvxx`, `lt_disjoint`,
-    `disjoint_neitv`, `neitv_bnd1`, `neitv_bnd2` (from `set_interval.v`)
-  + lemmas `setNK`, `lb_ubN`, `ub_lbN`, `mem_NE`, `nonemptyN`, `opp_set_eq0`,
-    `has_lb_ubN`, `has_ubPn`, `has_lbPn` (from `reals.v`)
-- in `classical_sets.v`:
-  + lemma `bigsetU_sup`
-- in `lebesgue_integral.v`:
-  + lemmas `emeasurable_fun_fsum`, `ge0_integral_fsum`
-- in `ereal.v`:
-  + lemma `fsumEFin`
-- in `lebesgue_measure.v`:
-  + definition `ErealGenInftyO.R` and lemma `ErealGenInftyO.measurableE`
-  + lemma `sub1set`
-- in `constructive_ereal.v`:
-  + lemmas `lteN10`, `leeN10`
-  + lemmas `le0_fin_numE`
-  + lemmas `fine_lt0`, `fine_le0`
-- in `sequences.v`:
-  + lemmas `is_cvg_ereal_npos_natsum_cond`, `lee_npeseries`,
-    `is_cvg_npeseries_cond`, `is_cvg_npeseries`, `npeseries_le0`,
-    `is_cvg_ereal_npos_natsum`
-  + lemma `nnseries_is_cvg`
-- in `constructive_ereal.v`:
-  + lemma `fine_lt0E`
-- in file `normedtype.v`
-  + lemmas `closed_ballR_compact` and `locally_compactR`
-
-- in `sequences.v`:
-  + lemma `invr_cvg0` and `invr_cvg_pinfty`
-  + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`,
-    `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
-- in `classical_sets.v`:
-  + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
-- in `classical_sets.v`:
-  + 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`
-
-- in `fsbig.v`:
-  + lemma `fsbig_setU_set1`
-- in `tooplogy.v`:
-  + lemmas `closed_bigsetU`, `accessible_finite_set_closed`
-
-
-- in file `classical_sets.v`,
-  + new lemma `preimage_range`.
-- in file `topology.v`,
-  + new lemmas `eq_cvg`, `eq_is_cvg`, `eq_near`, `cvg_toP`, `cvgNpoint`,
-    `filter_imply`, `nbhs_filter`, `near_fun`, `cvgnyPgt`, `cvgnyPgty`,
-    `cvgnyPgey`, `fcvg_ballP`, `fcvg_ball`, and `fcvg_ball2P`.
-- in `topology.v`, added `near do` and `near=> x do` tactic notations
-  to perform some tactics under a `\forall x \near F, ...` quantification.
-- in `normedtype.v`, added notations `^'+`, `^'-`, `+oo_R`, `-oo_R`
 
 - in file `topology.v`,
   + new definitions `quotient_topology`, and `quotient_open`.
   + new lemmas `pi_continuous`, `quotient_continuous`, and
     `repr_comp_continuous`.
 
-  + new definitions `hausdorff_accessible`, `separates_points_from_closed`, and 
+- in file `boolp.v`,
+  + new lemma `forallp_asboolPn2`.
+- in file `classical_sets.v`,
+  + new lemma `preimage_range`.
+- in file `topology.v`,
+  + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and 
     `join_product`.
   + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
     `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
-    `join_product_weak`.
-- in `boolp.v`:
-  + lemma `forallp_asboolPn2`
+    `join_product_weak`. 
 
 ### Changed
 
@@ -187,8 +97,6 @@
   + canonical `fimfun_comRingType`
   + lemma `max_fimfun_subproof`
   + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}`
-- in `topology.v`:
-  + `Topological.ax2`
 
 ### Renamed
 

From bc54f7aeaa040c434aeb14f53cd382869d37461b Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 6 Feb 2023 15:41:51 -0500
Subject: [PATCH 15/16] fixing build

---
 theories/topology.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/topology.v b/theories/topology.v
index 791ec0c5da..e6c4ea9f83 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3642,7 +3642,7 @@ split.
   case=> _; rewrite eqEsubset; case=> _ + x Ox => /(_ x I [set x]).
   by case; [by apply: open_nbhs_nbhs; split |] => y [+ _] => /[swap] -> /eqP.
 move=> NOx; split; [exact: closedT |]; rewrite eqEsubset; split => x // _.
-move=> U; rewrite nbhsE; case=> V [][] oV Vx VU.
+move=> U; rewrite nbhsE; case=> V [] oV Vx VU.
 have Vnx: V != [set x] by apply/eqP => M; apply: (NOx x); rewrite -M.
 have /existsNP [y /existsNP [Vy Ynx]] : ~ forall y, V y -> y = x.
   move/negP: Vnx; apply: contra_not => Vxy; apply/eqP; rewrite eqEsubset. 

From 6e5516b2f4fc8f3c4363e81e8ab7d9292859a185 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 6 Feb 2023 15:57:35 -0500
Subject: [PATCH 16/16] more build fixes

---
 theories/topology.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index e6c4ea9f83..b8ba388b9a 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3663,13 +3663,14 @@ Lemma perfect_diagonal (K : nat_topologicalType -> topologicalType) :
   (forall i, exists (xy: K i * K i), xy.1 != xy.2) ->
   perfect_set [set: product_topologicalType K].
 Proof.
-move=> npts; split; [exact: closedT|]; rewrite eqEsubset; split => f // _.
+move=> npts; split; first exact: closedT.
+rewrite eqEsubset; split => f // _.
 pose distincts (i : nat) := projT1 (sigW (npts i)).
 pose derange (i : nat) (z : K i) :=
   if z == (distincts i).1 then (distincts i).2 else (distincts i).1.
 pose g (N i : nat) := if (i < N)%nat then f i else derange _ (f i).
 have gcvg : g @ \oo --> (f : product_topologicalType K).
-  apply/(@cvg_sup (product_topologicalType K)) => N U [V] [[W] oW <-] [] WfN WU.
+  apply/(@cvg_sup (product_topologicalType K)) => N U [V] [][W] oW <- WfN WU.
   by apply: (filterS WU); rewrite nbhs_simpl /g; exists N.+1 => // i /= ->.
 move=> A /gcvg; rewrite nbhs_simpl; case=> N _ An.
 exists (g N); split => //; last by apply: An; rewrite /= ?leqnn //.