From 5225b3cf08cfd0f210eef67168ea1acf913f9e6f Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 16:15:28 -0400
Subject: [PATCH 01/14] proving sups preserve countable ent

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

diff --git a/theories/topology.v b/theories/topology.v
index 784341730c..3c9bd228c7 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2094,6 +2094,17 @@ rewrite predeqE => t; split=> [|fit]; first by apply; rewrite /= inE.
 by move=> ?; rewrite /= inE => /eqP->.
 Qed.
 
+Lemma finI_from_nat_bigcup T (f : nat -> set T) :
+  finI_from [set: nat] f = \bigcup_n (finI_from `I_n f).
+Proof.
+rewrite eqEsubset; split => E []; first last.
+  by move=> n _ [A An] <-; exists A => // ? _; rewrite mem_set.
+move=> A /= _; case : (pselect (A == fset0)).
+  by move=> /eqP ->; exists 0%N => //; exists fset0; rewrite // bigcap_set0.
+move=> /negP/fset_nat_maximum => /(_ id) [n] [nA] nub <-; exists n.+1 => //.
+by exists A => // k /nub ?; rewrite mem_set.
+Qed.
+
 Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) :
   countable D -> countable (finI_from D f).
 Proof.
@@ -2101,6 +2112,20 @@ move=> ?; apply: (card_le_trans (card_image_le _ _)).
 exact: fset_subset_countable.
 Qed.
 
+(*
+Lemma finI_from_comp (I J : pointedType) T (D : set I) 
+    (g : I -> J) (f : J -> set T) :
+  finI_from D (f \o g) = finI_from (g @` D) f.
+Proof.
+rewrite eqEsubset; split => E [A /=] Asub <-.
+  exists (g @` A)%fset.
+    move=> q /= /imfsetP [w /= wA ->]; rewrite mem_set //; exists w => //.
+    by apply: set_mem; exact: Asub.
+  rewrite eqEsubset; split => t It x /= Ax.
+    by apply: (It (g x)); rewrite mksetE; apply/imfsetP; exists x.
+  by have /imfsetP [w Aw ->] := Ax; apply: It.
+  *)
+
 Section TopologyOfSubbase.
 
 Variable (I : pointedType) (T : Type) (D : set I) (b : I -> set T).
@@ -4378,6 +4403,61 @@ Definition sup_uniformType := UniformType Tt sup_uniform_mixin.
 
 End sup_uniform.
 
+Section sup_uniform_countable.
+
+Variable (T : pointedType) (Tc : nat -> Uniform.class_of T).
+
+Let TS := fun i => Uniform.Pack (Tc i).
+Let Tt := @sup_uniformType T nat Tc.
+Let ent_of (p : nat * set (T*T)) := `[< @entourage (TS p.1) p.2>].
+Let IEnt := ChoiceType {p : ({classic nat} * set (T*T)) | ent_of p} (sig_choiceMixin _).
+
+Variable countable_ent : forall n, exists M : set (set (T * T)), 
+  countable M /\
+  (M `<=` @entourage (TS n)) /\ 
+  (forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P).
+
+Lemma countable_sup_ent : exists R,
+  countable R /\
+  (R `<=` @entourage Tt) /\ 
+  (forall P, @entourage Tt P -> exists Q, R Q /\ Q `<=` P).
+Proof.
+pose f := fun n => cid (countable_ent n).
+pose g : nat -> (set (set (T * T))) := fun n => projT1 (f n).
+exists (finI_from (\bigcup_n (g n)) id); split;[|split].
+- apply: finI_from_countable; apply: bigcup_countable => //.
+  by move=> i _; have []:= (projT2 (f i)).
+- rewrite /entourage /= /sup_ent /= => E [A /= AsubGn AE]; exists E => //.
+  have h : forall w, { p : IEnt | w \in A -> w = (projT1 p).2}.
+    move=> /= w; apply cid; case (pselect (w \in A)); first last.
+      by move=> ?; exists (exist ent_of _ (IEnt_pointT Tc 0%N)). 
+    move=> /[dup] /AsubGn/set_mem [n _ gnw] wA. 
+    have [_ [subE Ebase]] := projT2 (f n).
+    have ent : ent_of (n,w) by apply/asboolP; exact: (subE _ gnw).
+    by exists (exist ent_of (n, w) ent) => ?.
+  exists [fset (fun i => (projT1 (h i))) w | w in A]%fset.
+    by move=> ?; rewrite mem_set //.
+  rewrite -AE /=; rewrite eqEsubset; split => t Ia.
+    by move=> w Aw; have -> := (projT2 (h w) Aw); apply/Ia/imfsetP; exists w.
+  move=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia => //=.
+  suff <- : x = w by []; have -> := (projT2 (h x) xA).
+  have -> : (projT1 (proj1_sig (h x))) = (projT1 (exist ent_of (n, w) p)).
+    by rewrite M.
+  by have -> : (projT1 (exist ent_of (n, w) p)) = (n,w) by [].
+- move=> E [w] [/= A _ wIA wsubE]. 
+  have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
+    by move=> i; apply/asboolP; apply: (projT2 i).
+  pose h := fun i : IEnt => 
+    cid ((proj2 (proj2 (projT2 (f ((projT1 i).1))))) ((projT1 i).2) (ent_Ip i)).
+  pose AH := [fset (fun i => (projT1 (h i))) w | w in A]%fset.
+  exists (\bigcap_(i in [set` AH]) i); split.
+    exists AH => // p /= /imfsetP [i /= iA pE]; rewrite mem_set //.
+    by exists (projT1 i).1 => //; have [] := projT2 (h i); rewrite pE.
+  move=> t It; apply: wsubE; rewrite -wIA /= => i iA.
+  apply: It; apply/imfsetP; exists i => //.
+
+End sup_uniform_countable.
+
 Section product_uniform.
 
 Variable (I : choiceType) (T : I -> uniformType).

From da3025aa8875546f4c014a740dd6b31f95b9acdd Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 18:21:05 -0400
Subject: [PATCH 02/14] proof going through

---
 theories/topology.v | 65 +++++++++++++++++++++++----------------------
 1 file changed, 33 insertions(+), 32 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 3c9bd228c7..442c028041 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4401,62 +4401,63 @@ Definition sup_uniform_mixin:=
 
 Definition sup_uniformType := UniformType Tt sup_uniform_mixin.
 
-End sup_uniform.
-
-Section sup_uniform_countable.
-
-Variable (T : pointedType) (Tc : nat -> Uniform.class_of T).
-
-Let TS := fun i => Uniform.Pack (Tc i).
-Let Tt := @sup_uniformType T nat Tc.
-Let ent_of (p : nat * set (T*T)) := `[< @entourage (TS p.1) p.2>].
-Let IEnt := ChoiceType {p : ({classic nat} * set (T*T)) | ent_of p} (sig_choiceMixin _).
-
-Variable countable_ent : forall n, exists M : set (set (T * T)), 
-  countable M /\
-  (M `<=` @entourage (TS n)) /\ 
-  (forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P).
-
-Lemma countable_sup_ent : exists R,
+Lemma countable_sup_ent : 
+  countable [set: Ii] ->
+  (forall n, exists M : set (set (T * T)), 
+    countable M /\
+    (M `<=` @entourage (TS n)) /\ 
+    (forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P)) ->
+  exists R,
   countable R /\
-  (R `<=` @entourage Tt) /\ 
-  (forall P, @entourage Tt P -> exists Q, R Q /\ Q `<=` P).
+  (R `<=` @entourage sup_uniformType) /\ 
+  (forall P, @entourage sup_uniformType P -> exists Q, R Q /\ Q `<=` P).
 Proof.
+move=> Icnt countable_ent.
 pose f := fun n => cid (countable_ent n).
-pose g : nat -> (set (set (T * T))) := fun n => projT1 (f n).
+pose g : Ii -> set (set (T * T)) := fun n => projT1 (f n).
+case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
+  exists [set setT]; split; first apply countable1; split.
+    move=> A; rewrite /entourage /= => ->.
+    by exists setT => //; exists fset0 => //; rewrite set_fset0 bigcap_set0.
+  move=> P [w /= [A /= _]] <- subP; exists setT; split => //.
+  apply: (subset_trans _ subP) => t _ i iA.
+  by have : [set: I] (projT1 i).1 by []; rewrite I0.
 exists (finI_from (\bigcup_n (g n)) id); split;[|split].
-- apply: finI_from_countable; apply: bigcup_countable => //.
-  by move=> i _; have []:= (projT2 (f i)).
+- apply/finI_from_countable/bigcup_countable => // i _.
+  by have []:= (projT2 (f i)).
 - rewrite /entourage /= /sup_ent /= => E [A /= AsubGn AE]; exists E => //.
   have h : forall w, { p : IEnt | w \in A -> w = (projT1 p).2}.
-    move=> /= w; apply cid; case (pselect (w \in A)); first last.
-      by move=> ?; exists (exist ent_of _ (IEnt_pointT Tc 0%N)). 
+    move=> w; apply cid; case (pselect (w \in A)); first last.
+      by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)). 
     move=> /[dup] /AsubGn/set_mem [n _ gnw] wA. 
     have [_ [subE Ebase]] := projT2 (f n).
     have ent : ent_of (n,w) by apply/asboolP; exact: (subE _ gnw).
-    by exists (exist ent_of (n, w) ent) => ?.
+    by exists (exist ent_of (n, w) ent).
   exists [fset (fun i => (projT1 (h i))) w | w in A]%fset.
     by move=> ?; rewrite mem_set //.
   rewrite -AE /=; rewrite eqEsubset; split => t Ia.
-    by move=> w Aw; have -> := (projT2 (h w) Aw); apply/Ia/imfsetP; exists w.
+    by move=> w Aw; have -> := projT2 (h w) Aw; apply/Ia/imfsetP; exists w.
   move=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia => //=.
   suff <- : x = w by []; have -> := (projT2 (h x) xA).
-  have -> : (projT1 (proj1_sig (h x))) = (projT1 (exist ent_of (n, w) p)).
-    by rewrite M.
-  by have -> : (projT1 (exist ent_of (n, w) p)) = (n,w) by [].
+  by rewrite (_ : projT1 (h x) = proj1_sig (h x)) // -M //.
 - move=> E [w] [/= A _ wIA wsubE]. 
   have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
     by move=> i; apply/asboolP; apply: (projT2 i).
   pose h := fun i : IEnt => 
     cid ((proj2 (proj2 (projT2 (f ((projT1 i).1))))) ((projT1 i).2) (ent_Ip i)).
+  have ehi : forall i : IEnt, ent_of ((projT1 i).1, projT1 (h i)).
+    move=> i; apply/asboolP => /=; have [] := projT2 (h i).
+    have [_ [+ _] ? ?] := (projT2 (f (projT1 i).1)); exact.
   pose AH := [fset (fun i => (projT1 (h i))) w | w in A]%fset.
   exists (\bigcap_(i in [set` AH]) i); split.
     exists AH => // p /= /imfsetP [i /= iA pE]; rewrite mem_set //.
     by exists (projT1 i).1 => //; have [] := projT2 (h i); rewrite pE.
-  move=> t It; apply: wsubE; rewrite -wIA /= => i iA.
-  apply: It; apply/imfsetP; exists i => //.
+  apply: (subset_trans _ wsubE); rewrite -wIA => t It i Ai.
+  have [enthi] := (projT2 (h i)); apply; apply: It; apply/imfsetP.
+  by exists i .
+Qed.
 
-End sup_uniform_countable.
+End sup_uniform.
 
 Section product_uniform.
 

From 444642320e09590540ddb88b8a378b18b645e4a5 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 18:21:51 -0400
Subject: [PATCH 03/14] unused proofs

---
 theories/topology.v | 27 +--------------------------
 1 file changed, 1 insertion(+), 26 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 442c028041..0379f04454 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2094,17 +2094,6 @@ rewrite predeqE => t; split=> [|fit]; first by apply; rewrite /= inE.
 by move=> ?; rewrite /= inE => /eqP->.
 Qed.
 
-Lemma finI_from_nat_bigcup T (f : nat -> set T) :
-  finI_from [set: nat] f = \bigcup_n (finI_from `I_n f).
-Proof.
-rewrite eqEsubset; split => E []; first last.
-  by move=> n _ [A An] <-; exists A => // ? _; rewrite mem_set.
-move=> A /= _; case : (pselect (A == fset0)).
-  by move=> /eqP ->; exists 0%N => //; exists fset0; rewrite // bigcap_set0.
-move=> /negP/fset_nat_maximum => /(_ id) [n] [nA] nub <-; exists n.+1 => //.
-by exists A => // k /nub ?; rewrite mem_set.
-Qed.
-
 Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) :
   countable D -> countable (finI_from D f).
 Proof.
@@ -2112,20 +2101,6 @@ move=> ?; apply: (card_le_trans (card_image_le _ _)).
 exact: fset_subset_countable.
 Qed.
 
-(*
-Lemma finI_from_comp (I J : pointedType) T (D : set I) 
-    (g : I -> J) (f : J -> set T) :
-  finI_from D (f \o g) = finI_from (g @` D) f.
-Proof.
-rewrite eqEsubset; split => E [A /=] Asub <-.
-  exists (g @` A)%fset.
-    move=> q /= /imfsetP [w /= wA ->]; rewrite mem_set //; exists w => //.
-    by apply: set_mem; exact: Asub.
-  rewrite eqEsubset; split => t It x /= Ax.
-    by apply: (It (g x)); rewrite mksetE; apply/imfsetP; exists x.
-  by have /imfsetP [w Aw ->] := Ax; apply: It.
-  *)
-
 Section TopologyOfSubbase.
 
 Variable (I : pointedType) (T : Type) (D : set I) (b : I -> set T).
@@ -4454,7 +4429,7 @@ exists (finI_from (\bigcup_n (g n)) id); split;[|split].
     by exists (projT1 i).1 => //; have [] := projT2 (h i); rewrite pE.
   apply: (subset_trans _ wsubE); rewrite -wIA => t It i Ai.
   have [enthi] := (projT2 (h i)); apply; apply: It; apply/imfsetP.
-  by exists i .
+  by exists i.
 Qed.
 
 End sup_uniform.

From 90aff1f5f61ed41f2f2f720390e7b07479ec2736 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 18:45:25 -0400
Subject: [PATCH 04/14] linting

---
 theories/topology.v | 68 ++++++++++++++++++++++-----------------------
 1 file changed, 33 insertions(+), 35 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 0379f04454..b05ae7f393 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4376,59 +4376,57 @@ Definition sup_uniform_mixin:=
 
 Definition sup_uniformType := UniformType Tt sup_uniform_mixin.
 
-Lemma countable_sup_ent : 
+Lemma countable_sup_ent :
   countable [set: Ii] ->
   (forall n, exists M : set (set (T * T)), 
-    countable M /\
-    (M `<=` @entourage (TS n)) /\ 
-    (forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P)) ->
-  exists R,
-  countable R /\
-  (R `<=` @entourage sup_uniformType) /\ 
-  (forall P, @entourage sup_uniformType P -> exists Q, R Q /\ Q `<=` P).
-Proof.
-move=> Icnt countable_ent.
-pose f := fun n => cid (countable_ent n).
-pose g : Ii -> set (set (T * T)) := fun n => projT1 (f n).
+    [/\
+      countable M,
+      M `<=` @entourage (TS n) &
+      forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P]) ->
+  exists R, [/\
+    countable R,
+    R `<=` @entourage sup_uniformType &
+   forall P, @entourage sup_uniformType P -> exists Q, R Q /\ Q `<=` P].
+Proof.
+move=> Icnt countable_ent; pose f := fun n => cid (countable_ent n).
+pose g := fun n => projT1 (f n).
 case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
-  exists [set setT]; split; first apply countable1; split.
+  exists [set setT]; split; first apply countable1.
     move=> A; rewrite /entourage /= => ->.
     by exists setT => //; exists fset0 => //; rewrite set_fset0 bigcap_set0.
-  move=> P [w /= [A /= _]] <- subP; exists setT; split => //.
+  move=> P [w [A _]] <- subP; exists setT; split => //.
   apply: (subset_trans _ subP) => t _ i iA.
-  by have : [set: I] (projT1 i).1 by []; rewrite I0.
-exists (finI_from (\bigcup_n (g n)) id); split;[|split].
-- apply/finI_from_countable/bigcup_countable => // i _.
-  by have []:= (projT2 (f i)).
-- rewrite /entourage /= /sup_ent /= => E [A /= AsubGn AE]; exists E => //.
+  by suff : [set: I] (projT1 i).1 by rewrite I0.
+exists (finI_from (\bigcup_n (g n)) id); split.
+- by apply/finI_from_countable/bigcup_countable => // i _; case: (projT2 (f i)).
+- move=> E [A AsubGn AE]; exists E => //.
   have h : forall w, { p : IEnt | w \in A -> w = (projT1 p).2}.
-    move=> w; apply cid; case (pselect (w \in A)); first last.
-      by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)). 
+    move=> w; apply cid; case: (pselect (w \in A)); first last.
+      by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)).
     move=> /[dup] /AsubGn/set_mem [n _ gnw] wA. 
-    have [_ [subE Ebase]] := projT2 (f n).
-    have ent : ent_of (n,w) by apply/asboolP; exact: (subE _ gnw).
+    have [_ subE Ebase] := projT2 (f n).
+    have ent : ent_of (n,w) by apply/asboolP; exact: subE _ gnw.
     by exists (exist ent_of (n, w) ent).
-  exists [fset (fun i => (projT1 (h i))) w | w in A]%fset.
-    by move=> ?; rewrite mem_set //.
+  exists [fset (fun i => projT1 (h i)) w | w in A]%fset.
+    by move=> ?; rewrite mem_set.
   rewrite -AE /=; rewrite eqEsubset; split => t Ia.
     by move=> w Aw; have -> := projT2 (h w) Aw; apply/Ia/imfsetP; exists w.
-  move=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia => //=.
-  suff <- : x = w by []; have -> := (projT2 (h x) xA).
-  by rewrite (_ : projT1 (h x) = proj1_sig (h x)) // -M //.
-- move=> E [w] [/= A _ wIA wsubE]. 
+  case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia; rewrite (_ : w = x) //. 
+  by rewrite (projT2 (h x) xA) (_ : projT1 (h x) = proj1_sig (h x)) -M.
+- move=> E [w] [ A _ wIA wsubE]. 
   have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
     by move=> i; apply/asboolP; apply: (projT2 i).
-  pose h := fun i : IEnt => 
-    cid ((proj2 (proj2 (projT2 (f ((projT1 i).1))))) ((projT1 i).2) (ent_Ip i)).
+  pose h := fun i : IEnt =>
+    cid ((and3_rec (fun _ _ P => P) (projT2 (f ((projT1 i).1)))) ((projT1 i).2) (ent_Ip i)).
   have ehi : forall i : IEnt, ent_of ((projT1 i).1, projT1 (h i)).
     move=> i; apply/asboolP => /=; have [] := projT2 (h i).
-    have [_ [+ _] ? ?] := (projT2 (f (projT1 i).1)); exact.
+    by have [_ + _ ? ?] := (projT2 (f (projT1 i).1)); exact.
   pose AH := [fset (fun i => (projT1 (h i))) w | w in A]%fset.
   exists (\bigcap_(i in [set` AH]) i); split.
-    exists AH => // p /= /imfsetP [i /= iA pE]; rewrite mem_set //.
-    by exists (projT1 i).1 => //; have [] := projT2 (h i); rewrite pE.
+    exists AH => // p /imfsetP [i iA pE]; rewrite mem_set //.
+    by exists (projT1 i).1; have [] := projT2 (h i); rewrite // pE.
   apply: (subset_trans _ wsubE); rewrite -wIA => t It i Ai.
-  have [enthi] := (projT2 (h i)); apply; apply: It; apply/imfsetP.
+  have [?] := projT2 (h i); apply; apply: It; apply/imfsetP.
   by exists i.
 Qed.
 

From 9835fd83f88b1d0aab35ac5d2cc3ce4d95b93352 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 21:51:57 -0400
Subject: [PATCH 05/14] metric implies countable uniformity

---
 theories/topology.v | 63 ++++++++++++++++++++++++++++++++++++---------
 1 file changed, 51 insertions(+), 12 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index b05ae7f393..fbab19def9 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -285,6 +285,8 @@ Require Import reals signed.
 (*                   unif_continuous f <-> f is uniformly continuous.         *)
 (*               weak_uniformType == the uniform space for weak topologies    *)
 (*                sup_uniformType == the uniform space for sup topologies     *)
+(*         countable_uniformity T == T's entourage has a countable base. This *)
+(*                                   is equivalent to `T` being metrizable    *)
 (*                                                                            *)
 (* * PseudoMetric spaces :                                                    *)
 (*                entourage_ ball == entourages defined using balls           *)
@@ -4275,6 +4277,34 @@ Definition weak_uniformType :=
 
 End weak_uniform.
 
+Definition countable_uniformity (T : uniformType) :=
+  exists R : set (set (T * T)), [/\
+    countable R,
+    R `<=` entourage &
+   forall P, entourage P -> exists Q, R Q /\ Q `<=` P].
+
+Lemma countable_uniformityP {T : uniformType} : 
+  countable_uniformity T <-> 
+  (exists f : nat -> set (T * T), 
+   (forall A, entourage A -> exists N, f N `<=` A) 
+   /\
+  forall n, entourage (f n) 
+  ).
+Proof.
+split.
+  case=> M [] /pfcard_geP []. 
+    by move=> -> _ /(_ setT); case; [ exact: entourageT | move=> ? []].
+  move=> [f] entM Msub; exists f; split.
+    move=> ? /Msub [Q [MQ ?]]; have [n ? fQ] := (@surj _ _ _ _  f _ MQ).
+    by exists n; rewrite fQ.
+  by move=> n; apply: entM; apply: funS.
+case => f [fsubE] entf; exists (f@` [set: nat]); split.
+- exact: card_image_le.
+- by move=> E [n _] <-; exact: entf.
+- move=> E entE; have [n fnA] := fsubE _ entE.
+  by exists (f n); split => //; exists n.
+Qed.
+
 Section sup_uniform.
 
 Variable (T : pointedType) (Ii : Type) (Tc : Ii -> Uniform.class_of T).
@@ -4378,18 +4408,11 @@ Definition sup_uniformType := UniformType Tt sup_uniform_mixin.
 
 Lemma countable_sup_ent :
   countable [set: Ii] ->
-  (forall n, exists M : set (set (T * T)), 
-    [/\
-      countable M,
-      M `<=` @entourage (TS n) &
-      forall P, @entourage (TS n) P -> exists Q, M Q /\ Q `<=` P]) ->
-  exists R, [/\
-    countable R,
-    R `<=` @entourage sup_uniformType &
-   forall P, @entourage sup_uniformType P -> exists Q, R Q /\ Q `<=` P].
+  (forall n, countable_uniformity (TS n)) ->
+  countable_uniformity sup_uniformType.
 Proof.
 move=> Icnt countable_ent; pose f := fun n => cid (countable_ent n).
-pose g := fun n => projT1 (f n).
+pose g : Ii -> set (set (T * T)) := fun n => projT1 (f n).
 case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
   exists [set setT]; split; first apply countable1.
     move=> A; rewrite /entourage /= => ->.
@@ -4397,6 +4420,7 @@ case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
   move=> P [w [A _]] <- subP; exists setT; split => //.
   apply: (subset_trans _ subP) => t _ i iA.
   by suff : [set: I] (projT1 i).1 by rewrite I0.
+rewrite /countable_uniformity /=.
 exists (finI_from (\bigcup_n (g n)) id); split.
 - by apply/finI_from_countable/bigcup_countable => // i _; case: (projT2 (f i)).
 - move=> E [A AsubGn AE]; exists E => //.
@@ -4416,8 +4440,9 @@ exists (finI_from (\bigcup_n (g n)) id); split.
 - move=> E [w] [ A _ wIA wsubE]. 
   have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
     by move=> i; apply/asboolP; apply: (projT2 i).
-  pose h := fun i : IEnt =>
-    cid ((and3_rec (fun _ _ P => P) (projT2 (f ((projT1 i).1)))) ((projT1 i).2) (ent_Ip i)).
+  pose h : forall i : IEnt, {x : set (T * T) | _} := fun i : IEnt =>
+    cid ((and3_rec (fun _ _ P => P)
+      (projT2 (f ((projT1 i).1)))) ((projT1 i).2) (ent_Ip i)).
   have ehi : forall i : IEnt, ent_of ((projT1 i).1, projT1 (h i)).
     move=> i; apply/asboolP => /=; have [] := projT2 (h i).
     by have [_ + _ ? ?] := (projT2 (f (projT1 i).1)); exact.
@@ -4758,6 +4783,20 @@ by rewrite /unif_continuous -!entourage_ballE filter_fromP.
 Qed.
 End entourages.
 
+Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} :
+   countable_uniformity T.
+Proof.
+apply/countable_uniformityP; have ninvp : forall n, 0 < n.+1%:R^-1.
+  by move=> ? n; rewrite invr_gt0.
+exists (fun n => [set xy : T * T | ball xy.1 (PosNum (ninvp _ n))%:num xy.2]).
+split; last by move=> n; exact: entourage_ball.
+move=> E; rewrite -entourage_ballE => [[e]] ? subE.
+exists `|floor e^-1|%N; apply: (subset_trans _ subE) => xy; apply: le_ball.
+rewrite /= -{2}[e]invrK lef_pinv ?posrE ?invr_gt0 // ? natr_absz.
+apply: le_trans; first by apply: ltW; exact: lt_succ_floor.
+by rewrite -natr1 ler_add //= natr_absz ler_int ler_norm.
+Qed.
+
 (** ** Specific pseudoMetric spaces *)
 
 (** matrices *)

From 84109c7f52cbadee94d5ff3936e0b17d7e1bee48 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 21:54:56 -0400
Subject: [PATCH 06/14] fixing changelog

---
 CHANGELOG_UNRELEASED.md | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ec202fc3dd..2a3e197424 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,47 @@
 
 ### Added
 
+- in `topology.v`:
+  + lemmas `continuous_subspaceT`, `subspaceT_continuous`
+- in `constructive_ereal.v`
+  + lemmas `fine_le`, `fine_lt`, `fine_abse`, `abse_fin_num`
+- in `lebesgue_integral.v`
+  + lemmas `integral_fune_lt_pinfty`, `integral_fune_fin_num`
+- in `topology.v`
+  + lemma `weak_subspace_open`
+  + lemma `weak_ent_filter`, `weak_ent_refl`, `weak_ent_inv`, `weak_ent_split`,
+      `weak_ent_nbhs`
+  + definition `map_pair`, `weak_ent`, `weak_uniform_mixin`, `weak_uniformType`
+  + lemma `sup_ent_filter`, `sup_ent_refl`, `sup_ent_inv`, `sup_ent_split`,
+      `sup_ent_nbhs`
+  + definition `sup_ent`, `sup_uniform_mixin`, `sup_uniformType`
+  + definition `product_uniformType`
+  + lemma `uniform_entourage`
+  + definition `weak_ball`, `weak_pseudoMetricType`
+  + lemma `weak_ballE`
+  + lemma `finI_from_countable`
+  + definition `countable_uniformity`
+  + lemmas `countable_uniformityP`, `countable_sup_ent`,
+     `countable_uniformity_metric`
+- in `cardinality.v`
+  + lemmas `eq_card1`, `card_set1`, `card_eqSP`, `countable_n_subset`,
+     `countable_finite_subset`, `eq_card_fset_subset`, `fset_subset_countable`
+- in `classical_sets.v`
+  + lemmas `IIDn`, `IISl`
+- in `mathcomp_extra.v`
+  + lemma `lez_abs2n`
+- in `constructive_ereal.v`:
+  + lemmas `gte_addl`, `gte_addr`
+  + lemmas `gte_daddl`, `gte_daddr`
+  + lemma `lte_spadder`, `lte_spaddre`
+  + lemma `lte_spdadder`
+- in `constructive_ereal.v`:
+  + lemma `sum_fine`
+- in `topology.v`
+  + lemmas `entourage_invI`, `split_ent_subset`
+  + definition `countable_uniform_pseudoMetricType_mixin`
+- in `reals.v`:
+  + lemma `floor0`
 - in `classical_sets.v`:
   + canonical `unit_pointedType`
 - in `measure.v`:

From 39ab4e5b846a81e539c133a5c58cafce5666c2fb Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 3 Oct 2022 22:28:23 -0400
Subject: [PATCH 07/14] linting

---
 theories/topology.v | 53 +++++++++++++++++++++------------------------
 1 file changed, 25 insertions(+), 28 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index fbab19def9..6b0c12ebae 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3906,6 +3906,31 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Unshelve. all: by end_near. Qed.
 
+(* This property is primarily useful only for metrizability on uniform spaces *)
+Definition countable_uniformity (T : uniformType) :=
+  exists R : set (set (T * T)), [/\
+    countable R,
+    R `<=` entourage &
+    forall P, entourage P -> exists Q, R Q /\ Q `<=` P].
+
+Lemma countable_uniformityP {T : uniformType} : 
+  countable_uniformity T <-> exists f : nat -> set (T * T), 
+    (forall A, entourage A -> exists N, f N `<=` A) /\
+    (forall n, entourage (f n)).
+Proof.
+split.
+  case=> M [] /pfcard_geP []. 
+    by move=> -> _ /(_ setT); case; [exact: entourageT | move=> ? []].
+  move=> [f] eM Msub; exists f; split; last by move=> n; apply: eM; exact: funS.
+  move=> ? /Msub [Q [MQ ?]]; have [n ? fQ] := (@surj _ _ _ _  f _ MQ).
+  by exists n; rewrite fQ.
+case => f [fsubE] entf; exists (f @` [set: nat]); split.
+- exact: card_image_le.
+- by move=> E [n _] <-; exact: entf.
+- move=> E entE; have [n fnA] := fsubE _ entE.
+  by exists (f n); split => //; exists n.
+Qed.
+
 Section uniform_closeness.
 
 Variable (U : uniformType).
@@ -4277,34 +4302,6 @@ Definition weak_uniformType :=
 
 End weak_uniform.
 
-Definition countable_uniformity (T : uniformType) :=
-  exists R : set (set (T * T)), [/\
-    countable R,
-    R `<=` entourage &
-   forall P, entourage P -> exists Q, R Q /\ Q `<=` P].
-
-Lemma countable_uniformityP {T : uniformType} : 
-  countable_uniformity T <-> 
-  (exists f : nat -> set (T * T), 
-   (forall A, entourage A -> exists N, f N `<=` A) 
-   /\
-  forall n, entourage (f n) 
-  ).
-Proof.
-split.
-  case=> M [] /pfcard_geP []. 
-    by move=> -> _ /(_ setT); case; [ exact: entourageT | move=> ? []].
-  move=> [f] entM Msub; exists f; split.
-    move=> ? /Msub [Q [MQ ?]]; have [n ? fQ] := (@surj _ _ _ _  f _ MQ).
-    by exists n; rewrite fQ.
-  by move=> n; apply: entM; apply: funS.
-case => f [fsubE] entf; exists (f@` [set: nat]); split.
-- exact: card_image_le.
-- by move=> E [n _] <-; exact: entf.
-- move=> E entE; have [n fnA] := fsubE _ entE.
-  by exists (f n); split => //; exists n.
-Qed.
-
 Section sup_uniform.
 
 Variable (T : pointedType) (Ii : Type) (Tc : Ii -> Uniform.class_of T).

From b2238a5abf72fe7df3eab1300b5d5b53fe4487eb Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 21:27:11 -0400
Subject: [PATCH 08/14] metric for products

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

diff --git a/theories/topology.v b/theories/topology.v
index 6b0c12ebae..71effe9977 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -6094,11 +6094,19 @@ End weak_pseudoMetric.
    - infinite products of metric spaces are metrizable
 *)
 Section countable_uniform.
-Context {R : realType} {T : uniformType} (f_ : nat -> set (T * T)).
+Context {R : realType} {T : uniformType}.
 
-Hypothesis countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
+Hypothesis cnt_unif : @countable_uniformity T.
 
-Hypothesis entF : forall n, entourage (f_ n).
+Let f_ := projT1 (cid (iffLR countable_uniformityP cnt_unif)).
+
+Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
+Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
+
+Lemma entF : forall n, entourage (f_ n).
+Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
+
+#[local] Hint Resolve entF : core.
 
 (* Step 1:
    We build a nicer base `g` for `entourage` with better assumptions than `f`
@@ -6392,6 +6400,39 @@ Definition countable_uniform_pseudoMetricType_mixin := PseudoMetric.Mixin
 
 End countable_uniform.
 
+Section sup_pseudometric. 
+Variable (R : realType) (T : pointedType) (Ii : Type).
+Variable (Tc : Ii -> PseudoMetric.class_of R T).
+
+Hypothesis Icnt : countable [set: Ii].
+
+Let I : choiceType := classicType_choiceType Ii.
+Let TS := fun i => PseudoMetric.Pack (Tc i).
+
+Definition countable_uniformityT := (@countable_sup_ent T Ii Tc Icnt 
+    (fun i => @countable_uniformity_metric _ (TS i) )).
+
+Definition sup_pseudoMetric_mixin := @countable_uniform_pseudoMetricType_mixin R
+    (sup_uniformType Tc) countable_uniformityT.
+
+Definition sup_pseudoMetricType := 
+  PseudoMetricType (sup_uniformType Tc) sup_pseudoMetric_mixin.
+
+End sup_pseudometric.
+
+Section product_pseudometric.
+
+Variable (R : realType) (Ii : countType) (Tc : Ii -> pseudoMetricType R).
+
+Hypothesis Icnt : countable [set: Ii].
+
+Definition product_pseudoMetricType := 
+  sup_pseudoMetricType (fun i => PseudoMetric.class
+    (weak_pseudoMetricType (fun f : dep_arrow_pointedType Tc => f i)))
+    Icnt.
+
+End product_pseudometric.
+
 Definition subspace {T : Type} (A : set T) := T.
 Arguments subspace {T} _ : simpl never.
 
@@ -6651,7 +6692,7 @@ Global Instance subspace_proper_filter {T : topologicalType}
   (continuous (f : subspace A -> _)).*)
 Notation "{ 'within' A , 'continuous' f }" := (forall x,
   cvg_to [filter of fmap f (filter_of (Phantom (subspace A) x))]
-         [filter of f x]).
+         [filter of f x]) : classical_set_scope.
 
 Section SubspaceRelative.
 Context {T : topologicalType}.

From d7e316c379fd7446fc257ccaf73bd0f3dcaa1297 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 21:44:34 -0400
Subject: [PATCH 09/14] linting

---
 theories/topology.v | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 71effe9977..d1e57f36e1 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3913,22 +3913,20 @@ Definition countable_uniformity (T : uniformType) :=
     R `<=` entourage &
     forall P, entourage P -> exists Q, R Q /\ Q `<=` P].
 
-Lemma countable_uniformityP {T : uniformType} : 
-  countable_uniformity T <-> exists f : nat -> set (T * T), 
+Lemma countable_uniformityP {T : uniformType} :
+  countable_uniformity T <-> exists f : nat -> set (T * T),
     (forall A, entourage A -> exists N, f N `<=` A) /\
     (forall n, entourage (f n)).
 Proof.
 split.
-  case=> M [] /pfcard_geP []. 
+  case=> M [] /pfcard_geP [].
     by move=> -> _ /(_ setT); case; [exact: entourageT | move=> ? []].
   move=> [f] eM Msub; exists f; split; last by move=> n; apply: eM; exact: funS.
   move=> ? /Msub [Q [MQ ?]]; have [n ? fQ] := (@surj _ _ _ _  f _ MQ).
   by exists n; rewrite fQ.
-case => f [fsubE] entf; exists (f @` [set: nat]); split.
-- exact: card_image_le.
-- by move=> E [n _] <-; exact: entf.
-- move=> E entE; have [n fnA] := fsubE _ entE.
-  by exists (f n); split => //; exists n.
+case => f [fsubE] entf; exists (range f); split; first exact: card_image_le.
+  by move=> E [n _] <-; exact: entf.
+by move=> E /fsubE [n fnA]; exists (f n); split => //; exists n.
 Qed.
 
 Section uniform_closeness.
@@ -4404,21 +4402,19 @@ Definition sup_uniform_mixin:=
 Definition sup_uniformType := UniformType Tt sup_uniform_mixin.
 
 Lemma countable_sup_ent :
-  countable [set: Ii] ->
-  (forall n, countable_uniformity (TS n)) ->
+  countable [set: Ii] -> (forall n, countable_uniformity (TS n)) ->
   countable_uniformity sup_uniformType.
 Proof.
 move=> Icnt countable_ent; pose f := fun n => cid (countable_ent n).
 pose g : Ii -> set (set (T * T)) := fun n => projT1 (f n).
 case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
-  exists [set setT]; split; first apply countable1.
+  exists [set setT]; split; first exact: countable1.
     move=> A; rewrite /entourage /= => ->.
     by exists setT => //; exists fset0 => //; rewrite set_fset0 bigcap_set0.
   move=> P [w [A _]] <- subP; exists setT; split => //.
   apply: (subset_trans _ subP) => t _ i iA.
   by suff : [set: I] (projT1 i).1 by rewrite I0.
-rewrite /countable_uniformity /=.
-exists (finI_from (\bigcup_n (g n)) id); split.
+rewrite /countable_uniformity /=; exists (finI_from (\bigcup_n g n) id); split.
 - by apply/finI_from_countable/bigcup_countable => // i _; case: (projT2 (f i)).
 - move=> E [A AsubGn AE]; exists E => //.
   have h : forall w, { p : IEnt | w \in A -> w = (projT1 p).2}.
@@ -4432,7 +4428,7 @@ exists (finI_from (\bigcup_n (g n)) id); split.
     by move=> ?; rewrite mem_set.
   rewrite -AE /=; rewrite eqEsubset; split => t Ia.
     by move=> w Aw; have -> := projT2 (h w) Aw; apply/Ia/imfsetP; exists w.
-  case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia; rewrite (_ : w = x) //. 
+  case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia; rewrite (_ : w = x) //.
   by rewrite (projT2 (h x) xA) (_ : projT1 (h x) = proj1_sig (h x)) -M.
 - move=> E [w] [ A _ wIA wsubE]. 
   have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
@@ -4447,7 +4443,7 @@ exists (finI_from (\bigcup_n (g n)) id); split.
   exists (\bigcap_(i in [set` AH]) i); split.
     exists AH => // p /imfsetP [i iA pE]; rewrite mem_set //.
     by exists (projT1 i).1; have [] := projT2 (h i); rewrite // pE.
-  apply: (subset_trans _ wsubE); rewrite -wIA => t It i Ai.
+  apply: (subset_trans _ wsubE); rewrite -wIA => ? It i ?.
   have [?] := projT2 (h i); apply; apply: It; apply/imfsetP.
   by exists i.
 Qed.

From d9112db40db8f95880ea36e52c8412d22d5f4d77 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 6 Oct 2022 22:06:37 -0400
Subject: [PATCH 10/14] fixing docs

---
 CHANGELOG_UNRELEASED.md | 131 ++++++++++++++++++++++++++++++++++++++++
 theories/topology.v     |   5 +-
 2 files changed, 134 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2a3e197424..317052e97f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -100,6 +100,137 @@
 - in `functions.v`:
   + lemma `countable_bijP`
   + lemma `patchE`
+  + 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 `topoogy.v`
+  + definitions `sup_pseudoMetricType`, `product_pseudoMetricType`
+
+- 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 `constructive_ereal.v`:
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`
diff --git a/theories/topology.v b/theories/topology.v
index d1e57f36e1..d43936715d 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -367,6 +367,7 @@ Require Import reals signed.
 (*                                                                            *)
 (* We endow several standard types with the types of topological notions:     *)
 (* - products: prod_topologicalType, prod_uniformType, prod_pseudoMetricType  *)
+(*     sup_pseudoMetricType, weak_pseudoMetricType, product_pseudoMetricType  *)
 (* - matrices: matrix_filtered, matrix_topologicalType, matrix_uniformType,   *)
 (*     matrix_pseudoMetricType, matrix_completeType,                          *)
 (*     matrix_completePseudoMetricType                                        *)
@@ -6096,10 +6097,10 @@ Hypothesis cnt_unif : @countable_uniformity T.
 
 Let f_ := projT1 (cid (iffLR countable_uniformityP cnt_unif)).
 
-Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
+Local Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
 Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
 
-Lemma entF : forall n, entourage (f_ n).
+Local Lemma entF : forall n, entourage (f_ n).
 Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
 
 #[local] Hint Resolve entF : core.

From f86a8d523fd8ac0733dd388e928dc1ad7955b5bf Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 22 Nov 2022 21:56:40 +0900
Subject: [PATCH 11/14] use %:pos

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

diff --git a/theories/topology.v b/theories/topology.v
index d43936715d..feadb7a434 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4778,14 +4778,13 @@ Qed.
 End entourages.
 
 Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} :
-   countable_uniformity T.
+  countable_uniformity T.
 Proof.
-apply/countable_uniformityP; have ninvp : forall n, 0 < n.+1%:R^-1.
-  by move=> ? n; rewrite invr_gt0.
-exists (fun n => [set xy : T * T | ball xy.1 (PosNum (ninvp _ n))%:num xy.2]).
-split; last by move=> n; exact: entourage_ball.
+apply/countable_uniformityP.
+exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]).
+split; last by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos).
 move=> E; rewrite -entourage_ballE => [[e]] ? subE.
-exists `|floor e^-1|%N; apply: (subset_trans _ subE) => xy; apply: le_ball.
+exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball.
 rewrite /= -{2}[e]invrK lef_pinv ?posrE ?invr_gt0 // ? natr_absz.
 apply: le_trans; first by apply: ltW; exact: lt_succ_floor.
 by rewrite -natr1 ler_add //= natr_absz ler_int ler_norm.

From 95b9ac8051a4744f3d2bf5e2476a623e81ddca5f Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 2 Jan 2023 13:36:46 -0500
Subject: [PATCH 12/14] fixing changelog

---
 CHANGELOG_UNRELEASED.md | 52 ++++-------------------------------------
 1 file changed, 5 insertions(+), 47 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 317052e97f..1b066438d1 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,47 +4,6 @@
 
 ### Added
 
-- in `topology.v`:
-  + lemmas `continuous_subspaceT`, `subspaceT_continuous`
-- in `constructive_ereal.v`
-  + lemmas `fine_le`, `fine_lt`, `fine_abse`, `abse_fin_num`
-- in `lebesgue_integral.v`
-  + lemmas `integral_fune_lt_pinfty`, `integral_fune_fin_num`
-- in `topology.v`
-  + lemma `weak_subspace_open`
-  + lemma `weak_ent_filter`, `weak_ent_refl`, `weak_ent_inv`, `weak_ent_split`,
-      `weak_ent_nbhs`
-  + definition `map_pair`, `weak_ent`, `weak_uniform_mixin`, `weak_uniformType`
-  + lemma `sup_ent_filter`, `sup_ent_refl`, `sup_ent_inv`, `sup_ent_split`,
-      `sup_ent_nbhs`
-  + definition `sup_ent`, `sup_uniform_mixin`, `sup_uniformType`
-  + definition `product_uniformType`
-  + lemma `uniform_entourage`
-  + definition `weak_ball`, `weak_pseudoMetricType`
-  + lemma `weak_ballE`
-  + lemma `finI_from_countable`
-  + definition `countable_uniformity`
-  + lemmas `countable_uniformityP`, `countable_sup_ent`,
-     `countable_uniformity_metric`
-- in `cardinality.v`
-  + lemmas `eq_card1`, `card_set1`, `card_eqSP`, `countable_n_subset`,
-     `countable_finite_subset`, `eq_card_fset_subset`, `fset_subset_countable`
-- in `classical_sets.v`
-  + lemmas `IIDn`, `IISl`
-- in `mathcomp_extra.v`
-  + lemma `lez_abs2n`
-- in `constructive_ereal.v`:
-  + lemmas `gte_addl`, `gte_addr`
-  + lemmas `gte_daddl`, `gte_daddr`
-  + lemma `lte_spadder`, `lte_spaddre`
-  + lemma `lte_spdadder`
-- in `constructive_ereal.v`:
-  + lemma `sum_fine`
-- in `topology.v`
-  + lemmas `entourage_invI`, `split_ent_subset`
-  + definition `countable_uniform_pseudoMetricType_mixin`
-- in `reals.v`:
-  + lemma `floor0`
 - in `classical_sets.v`:
   + canonical `unit_pointedType`
 - in `measure.v`:
@@ -225,12 +184,11 @@
 - 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`
+  + new definitions `countable_uniformity`, `countable_uniformityT`, 
+    `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and 
+    `product_pseudoMetricType`.
+  + new lemmas `countable_uniformityP`, `countable_sup_ent`, and 
+    `countable_uniformity_metric`.
 
 - in `constructive_ereal.v`:
   + lemmas `adde_def_doppeD`, `adde_def_doppeB`

From 68c8faa9689c2bc9dba29607da0916addc2c7329 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Fri, 27 Jan 2023 22:49:23 -0500
Subject: [PATCH 13/14] fix changelog

---
 CHANGELOG_UNRELEASED.md | 123 ----------------------------------------
 1 file changed, 123 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1b066438d1..1d842d6fdb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -59,130 +59,7 @@
 - in `functions.v`:
   + lemma `countable_bijP`
   + lemma `patchE`
-  + 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 `topoogy.v`
-  + definitions `sup_pseudoMetricType`, `product_pseudoMetricType`
-
-- 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 definitions `countable_uniformity`, `countable_uniformityT`, 
     `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and 

From 6ec0f0958010b578982c11aff1efa10a91923ddb Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 7 Feb 2023 18:46:12 +0900
Subject: [PATCH 14/14] nitpicking

---
 theories/lebesgue_measure.v |   3 +-
 theories/real_interval.v    |   6 +-
 theories/topology.v         | 132 ++++++++++++++++--------------------
 3 files changed, 63 insertions(+), 78 deletions(-)

diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index a6de824911..1e123ee155 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -384,8 +384,7 @@ exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
   apply/esym; rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.
   rewrite in_itv/= !natr_absz intr_norm intrD.
   suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
-  rewrite [ltRHS]ger0_norm//; last by rewrite addr_ge0// ler0z floor_ge0.
-  by rewrite (le_lt_trans _ (lt_succ_floor _)) ?ler_norm.
+  by rewrite ger0_norm ?addr_ge0 ?ler0z ?floor_ge0// lt_succ_floor.
 by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry.
 Qed.
 
diff --git a/theories/real_interval.v b/theories/real_interval.v
index 8ca4e888b0..257386fd71 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -175,10 +175,10 @@ Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
 Proof.
 rewrite predeqE => y; split=> /=; last first.
   by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy.
-rewrite in_itv /= andbT => xy; exists (`|floor y|%N.+1) => //=.
-rewrite in_itv /= xy /= -natr1.
+rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=.
+rewrite in_itv /= xy /=.
 have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_spaddr.
-by rewrite natr_absz ger0_norm ?lt_succ_floor// floor_ge0 ltW.
+by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
diff --git a/theories/topology.v b/theories/topology.v
index feadb7a434..747168f662 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2078,7 +2078,7 @@ End TopologyOfBase.
 (** ** Topology defined by a subbase of open sets *)
 
 Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) :=
-  [set \bigcap_(i in [set i | i \in D']) f i |
+  [set \bigcap_(i in [set` D']) f i |
     D' in [set A : {fset I} | {subset A <= D}]].
 
 Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) :
@@ -3912,22 +3912,20 @@ Definition countable_uniformity (T : uniformType) :=
   exists R : set (set (T * T)), [/\
     countable R,
     R `<=` entourage &
-    forall P, entourage P -> exists Q, R Q /\ Q `<=` P].
+    forall P, entourage P -> exists2 Q, R Q & Q `<=` P].
 
 Lemma countable_uniformityP {T : uniformType} :
-  countable_uniformity T <-> exists f : nat -> set (T * T),
-    (forall A, entourage A -> exists N, f N `<=` A) /\
+  countable_uniformity T <-> exists2 f : nat -> set (T * T),
+    (forall A, entourage A -> exists N, f N `<=` A) &
     (forall n, entourage (f n)).
 Proof.
-split.
-  case=> M [] /pfcard_geP [].
-    by move=> -> _ /(_ setT); case; [exact: entourageT | move=> ? []].
-  move=> [f] eM Msub; exists f; split; last by move=> n; apply: eM; exact: funS.
-  move=> ? /Msub [Q [MQ ?]]; have [n ? fQ] := (@surj _ _ _ _  f _ MQ).
-  by exists n; rewrite fQ.
-case => f [fsubE] entf; exists (range f); split; first exact: card_image_le.
+split=> [[M []]|[f fsubE entf]].
+  move=> /pfcard_geP[-> _ /(_ _ entourageT)[]//|/unsquash f eM Msub].
+  exists f; last by move=> n; apply: eM; exact: funS.
+  by move=> ? /Msub [Q + ?] => /(@surj _ _ _ _ f)[n _ fQ]; exists n; rewrite fQ.
+exists (range f); split; first exact: card_image_le.
   by move=> E [n _] <-; exact: entf.
-by move=> E /fsubE [n fnA]; exists (f n); split => //; exists n.
+by move=> E /fsubE [n fnA]; exists (f n) => //; exists n.
 Qed.
 
 Section uniform_closeness.
@@ -4406,47 +4404,41 @@ Lemma countable_sup_ent :
   countable [set: Ii] -> (forall n, countable_uniformity (TS n)) ->
   countable_uniformity sup_uniformType.
 Proof.
-move=> Icnt countable_ent; pose f := fun n => cid (countable_ent n).
-pose g : Ii -> set (set (T * T)) := fun n => projT1 (f n).
-case (pselect ([set: I] = set0)) => [I0 | /eqP/set0P [i0 _]].
-  exists [set setT]; split; first exact: countable1.
-    move=> A; rewrite /entourage /= => ->.
-    by exists setT => //; exists fset0 => //; rewrite set_fset0 bigcap_set0.
-  move=> P [w [A _]] <- subP; exists setT; split => //.
-  apply: (subset_trans _ subP) => t _ i iA.
+move=> Icnt countable_ent; pose f n := cid (countable_ent n).
+pose g (n : Ii) : set (set (T * T)) := projT1 (f n).
+have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0.
+  exists [set setT]; split; [exact: countable1|move=> A ->; exact: entourageT|].
+  move=> P [w [A _]] <- subP; exists setT => //.
+  apply: subset_trans subP; apply: sub_bigcap => i _ ? _.
   by suff : [set: I] (projT1 i).1 by rewrite I0.
-rewrite /countable_uniformity /=; exists (finI_from (\bigcup_n g n) id); split.
-- by apply/finI_from_countable/bigcup_countable => // i _; case: (projT2 (f i)).
+exists (finI_from (\bigcup_n g n) id); split.
+- by apply/finI_from_countable/bigcup_countable => //i _; case: (projT2 (f i)).
 - move=> E [A AsubGn AE]; exists E => //.
-  have h : forall w, { p : IEnt | w \in A -> w = (projT1 p).2}.
-    move=> w; apply cid; case: (pselect (w \in A)); first last.
-      by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)).
-    move=> /[dup] /AsubGn/set_mem [n _ gnw] wA. 
-    have [_ subE Ebase] := projT2 (f n).
-    have ent : ent_of (n,w) by apply/asboolP; exact: subE _ gnw.
-    by exists (exist ent_of (n, w) ent).
-  exists [fset (fun i => projT1 (h i)) w | w in A]%fset.
-    by move=> ?; rewrite mem_set.
-  rewrite -AE /=; rewrite eqEsubset; split => t Ia.
-    by move=> w Aw; have -> := projT2 (h w) Aw; apply/Ia/imfsetP; exists w.
-  case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia; rewrite (_ : w = x) //.
-  by rewrite (projT2 (h x) xA) (_ : projT1 (h x) = proj1_sig (h x)) -M.
-- move=> E [w] [ A _ wIA wsubE]. 
-  have ent_Ip : forall (i : IEnt), @entourage (TS (projT1 i).1) (projT1 i).2.
-    by move=> i; apply/asboolP; apply: (projT2 i).
-  pose h : forall i : IEnt, {x : set (T * T) | _} := fun i : IEnt =>
-    cid ((and3_rec (fun _ _ P => P)
-      (projT2 (f ((projT1 i).1)))) ((projT1 i).2) (ent_Ip i)).
-  have ehi : forall i : IEnt, ent_of ((projT1 i).1, projT1 (h i)).
-    move=> i; apply/asboolP => /=; have [] := projT2 (h i).
-    by have [_ + _ ? ?] := (projT2 (f (projT1 i).1)); exact.
-  pose AH := [fset (fun i => (projT1 (h i))) w | w in A]%fset.
-  exists (\bigcap_(i in [set` AH]) i); split.
-    exists AH => // p /imfsetP [i iA pE]; rewrite mem_set //.
-    by exists (projT1 i).1; have [] := projT2 (h i); rewrite // pE.
-  apply: (subset_trans _ wsubE); rewrite -wIA => ? It i ?.
-  have [?] := projT2 (h i); apply; apply: It; apply/imfsetP.
-  by exists i.
+  have h (w : set (T * T)) : { p : IEnt | w \in A -> w = (projT1 p).2 }.
+    apply cid; have [|] := boolP (w \in A); last first.
+      by exists (exist ent_of _ (IEnt_pointT i0)).
+    move=> /[dup] /AsubGn /set_mem [n _ gnw] wA.
+    suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent).
+    by apply/asboolP; have [_ + _] := projT2 (f n); exact.
+  exists [fset sval (h w) | w in A]%fset; first by move=> ?; exact: in_setT.
+  rewrite -AE; rewrite eqEsubset; split => t Ia.
+    by move=> w Aw; rewrite (svalP (h w) Aw); apply/Ia/imfsetP; exists w.
+  case=> [[n w]] p /imfsetP [x /= xA M]; apply: Ia.
+  by rewrite (_ : w = x) // (svalP (h x) xA) -M.
+- move=> E [w] [ A _ wIA wsubE].
+  have ent_Ip (i : IEnt) : @entourage (TS (projT1 i).1) (projT1 i).2.
+    by apply/asboolP; exact: (projT2 i).
+  pose h (i : IEnt) : {x : set (T * T) | _} := cid2 (and3_rec
+    (fun _ _ P => P) (projT2 (f (projT1 i).1)) (projT1 i).2 (ent_Ip i)).
+  have ehi (i : IEnt) : ent_of ((projT1 i).1, projT1 (h i)).
+    apply/asboolP => /=; have [] := projT2 (h i).
+    by have [_ + _ ? ?] := projT2 (f (projT1 i).1); exact.
+  pose AH := [fset projT1 (h w) | w in A]%fset.
+  exists (\bigcap_(i in [set` AH]) i).
+    exists AH => // p /imfsetP [i iA ->]; rewrite inE //.
+    by exists (projT1 i).1 => //; have [] := projT2 (h i).
+  apply: subset_trans wsubE; rewrite -wIA => ? It i ?.
+  by have [?] := projT2 (h i); apply; apply: It; apply/imfsetP; exists i.
 Qed.
 
 End sup_uniform.
@@ -4781,13 +4773,12 @@ Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} :
   countable_uniformity T.
 Proof.
 apply/countable_uniformityP.
-exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]).
-split; last by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos).
-move=> E; rewrite -entourage_ballE => [[e]] ? subE.
+exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first.
+  by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos).
+move=> E; rewrite -entourage_ballE => -[e e0 subE].
 exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball.
-rewrite /= -{2}[e]invrK lef_pinv ?posrE ?invr_gt0 // ? natr_absz.
-apply: le_trans; first by apply: ltW; exact: lt_succ_floor.
-by rewrite -natr1 ler_add //= natr_absz ler_int ler_norm.
+rewrite /= -[leRHS]invrK lef_pinv ?posrE ?invr_gt0// -natr1.
+by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor.
 Qed.
 
 (** ** Specific pseudoMetric spaces *)
@@ -6094,15 +6085,13 @@ Context {R : realType} {T : uniformType}.
 
 Hypothesis cnt_unif : @countable_uniformity T.
 
-Let f_ := projT1 (cid (iffLR countable_uniformityP cnt_unif)).
+Let f_ := projT1 (cid2 (iffLR countable_uniformityP cnt_unif)).
 
 Local Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
-Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
+Proof. by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.
 
-Local Lemma entF : forall n, entourage (f_ n).
-Proof. by have [] := projT2 (cid (iffLR countable_uniformityP cnt_unif)). Qed.
-
-#[local] Hint Resolve entF : core.
+Let entF : forall n, entourage (f_ n).
+Proof. by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.
 
 (* Step 1:
    We build a nicer base `g` for `entourage` with better assumptions than `f`
@@ -6115,14 +6104,12 @@ Local Fixpoint g_ (n : nat) : set (T * T) :=
   if n is S n then let W := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1
   else [set: T*T].
 
-Local Lemma entG (n : nat) : entourage (g_ n).
+Let entG (n : nat) : entourage (g_ n).
 Proof.
 elim: n => /=; first exact: entourageT.
 by move=> n entg; apply/entourage_invI; exact: filterI.
 Qed.
 
-#[local] Hint Resolve entG : core.
-
 Local Lemma symG (n : nat) : ((g_ n)^-1)%classic = g_ n.
 Proof.
 by case: n => // n; rewrite eqEsubset; split; case=> ? ?; rewrite /= andC.
@@ -6396,7 +6383,7 @@ Definition countable_uniform_pseudoMetricType_mixin := PseudoMetric.Mixin
 
 End countable_uniform.
 
-Section sup_pseudometric. 
+Section sup_pseudometric.
 Variable (R : realType) (T : pointedType) (Ii : Type).
 Variable (Tc : Ii -> PseudoMetric.class_of R T).
 
@@ -6405,24 +6392,23 @@ Hypothesis Icnt : countable [set: Ii].
 Let I : choiceType := classicType_choiceType Ii.
 Let TS := fun i => PseudoMetric.Pack (Tc i).
 
-Definition countable_uniformityT := (@countable_sup_ent T Ii Tc Icnt 
-    (fun i => @countable_uniformity_metric _ (TS i) )).
+Definition countable_uniformityT := @countable_sup_ent T Ii Tc Icnt
+  (fun i => @countable_uniformity_metric _ (TS i)).
 
 Definition sup_pseudoMetric_mixin := @countable_uniform_pseudoMetricType_mixin R
-    (sup_uniformType Tc) countable_uniformityT.
+  (sup_uniformType Tc) countable_uniformityT.
 
-Definition sup_pseudoMetricType := 
+Definition sup_pseudoMetricType :=
   PseudoMetricType (sup_uniformType Tc) sup_pseudoMetric_mixin.
 
 End sup_pseudometric.
 
 Section product_pseudometric.
-
 Variable (R : realType) (Ii : countType) (Tc : Ii -> pseudoMetricType R).
 
 Hypothesis Icnt : countable [set: Ii].
 
-Definition product_pseudoMetricType := 
+Definition product_pseudoMetricType :=
   sup_pseudoMetricType (fun i => PseudoMetric.class
     (weak_pseudoMetricType (fun f : dep_arrow_pointedType Tc => f i)))
     Icnt.