From aa9c91f2d6a5b35f4601b61ecc50fb0f86378a0e Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 3 Oct 2024 22:56:06 -0400
Subject: [PATCH 1/7] more splitting or topology

---
 _CoqProject                  |    1 +
 theories/cantor.v            |    1 +
 theories/derive.v            |    1 +
 theories/function_spaces.v   |    4 +-
 theories/normedtype.v        |    2 +
 theories/separation_axioms.v | 1060 ++++++++++++++++++++++++++++++++++
 theories/topology.v          | 1000 +-------------------------------
 7 files changed, 1070 insertions(+), 999 deletions(-)
 create mode 100644 theories/separation_axioms.v

diff --git a/_CoqProject b/_CoqProject
index 3ef7b7c49..4261f8dcb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,6 +27,7 @@ theories/reals.v
 theories/landau.v
 theories/Rstruct.v
 theories/topology.v
+theories/separation_axioms.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v
diff --git a/theories/cantor.v b/theories/cantor.v
index c06d4f72e..5408b00d7 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -4,6 +4,7 @@ From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
 From mathcomp Require Import reals signed topology function_spaces.
+From mathcomp Require Import separation_axioms.
 From HB Require Import structures.
 
 (**md**************************************************************************)
diff --git a/theories/derive.v b/theories/derive.v
index 9f97fe633..bb68f56c8 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -3,6 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
+Require Import separation_axioms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index bacf96594..fcc1a68e8 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-Require Import reals signed topology.
+Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
@@ -1421,7 +1421,7 @@ Lemma continuous_uncurry (f : U -> V -> W) :
 Proof.
 move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //.
 move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB].
-by move=> z; exact: (@compact_regular V hsdf v B).
+by move=> z; exact: (compact_regular _ cptB).
 Qed.
 
 Lemma curry_continuous (f : (U * V)%type -> W) : continuous f -> @regular_space U ->
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 52f4ee754..4bd8b27fc 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -6,6 +6,8 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
+Require Import separation_axioms.
+Require Export separation_axioms.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
new file mode 100644
index 000000000..847b22641
--- /dev/null
+++ b/theories/separation_axioms.v
@@ -0,0 +1,1060 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
+From mathcomp Require Import archimedean.
+From mathcomp Require Import boolp classical_sets functions wochoice.
+From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
+From mathcomp Require Import filter reals signed topology.
+From mathcomp Require Export topology.
+
+(**md**************************************************************************)
+(* # Separation Axioms                                                        *)
+(*                                                                            *)
+(* This file introduces the separation axioms, a series of topological        *)
+(* properties about separating points and sets. They are somtimes denoted by  *)
+(* the names T0 through T6. Although we use their full names (hausdorff,      *)
+(* accessible, uniform, etc). This file also provides related topological     *)
+(* properties like zero dimensional and perfect, and discrete.                *)
+(*                                                                            *)
+(*              set_nbhs A == filter from open sets containing A              *)    
+(* ## The classic separation axioms                                           *)
+(* ```                                                                        *)
+(*      kolmogorov_space T == T is a Kolmogorov space (T0)                    *)
+(*      accessible_space T == T is an accessible space (T1)                   *)
+(*       hausdorff_space T == T is a Hausdorff space (T2)                     *)
+(*               close x y == x and y are arbitrarily close w.r.t. open sets  *)
+(*          normal_space T == T is normal (sometimes called T4)               *)
+(*         regular_space T == T is regular (sometimes called T3)              *)
+(* ```                                                                        *)
+(* ## related concepts                                                        *)
+(* ```                                                                        *)
+(*  totally_disconnected A == the only connected subsets of A are             *)
+(*                            empty or singletons                             *)
+(*      zero_dimensional T == points are separable by a clopen set            *)
+(*           perfect_set A == A is closed, and every point in A is            *)
+(*                            a limit point of A                              *)
+(* ```                                                                        *)
+(* ## metrizability for uniform spaces                                        *)
+(* ```                                                                        *)
+(*  countable_uniform.type == endows a pseudoMetric on a uniform type whose   *)
+(*                            entourage has a countable basis                 *)
+(*                 gauge E == for an entourage E, gauge E is a filter which   *)
+(*                            includes `iter n split_ent E`.                  *)
+(*                            Critically, `gauge E` forms a uniform space     *)
+(*                            with a countable uniformity.                    *)
+(*        sup_pseudometric == the pseudometric induced for the supremum       *)
+(*                            of countably many pseudoMetrics                 *)
+(******************************************************************************)
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(* Making sure that [Program] does not automatically introduce *)
+Obligation Tactic := idtac.
+
+Import Order.TTheory GRing.Theory Num.Theory.
+From mathcomp Require Import mathcomp_extra.
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Section set_nbhs.
+Context {T : topologicalType} (A : set T).
+
+Definition set_nbhs := \bigcap_(x in A) nbhs x.
+
+Global Instance set_nbhs_filter : Filter set_nbhs.
+Proof.
+split => P Q; first by exact: filterT.
+  by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx].
+by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact.
+Qed.
+
+Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs.
+Proof.
+case=> x Ax; split; last exact: set_nbhs_filter.
+by move/(_ x Ax)/nbhs_singleton.
+Qed.
+
+Lemma set_nbhsP (B : set T) :
+   set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]).
+Proof.
+split; first last.
+  by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs.
+move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B].
+  have [/snB|?] := pselect (A x); last by exists point.
+  by rewrite nbhsE => -[V [? ? ?]]; exists V.
+exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split.
+- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)).
+- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)).
+- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact.
+Qed.
+
+End set_nbhs.
+
+Section point_separation_axioms.
+Context {T : topologicalType}.
+
+
+Definition accessible_space := forall x y, x != y ->
+  exists A : set T, open A /\ x \in A /\ y \in ~` A.
+
+Definition kolmogorov_space := forall x y, x != y ->
+  exists A : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).
+
+Definition hausdorff_space := forall p q : T, cluster (nbhs p) q -> p = q.
+
+Lemma compact_closed (A : set T) : hausdorff_space -> compact A -> closed A.
+Proof.
+move=> hT Aco p clAp; have pA := !! @withinT _ (nbhs p) A _.
+have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //.
+by apply: cvg_cluster clsAp_q; apply: cvg_within.
+Qed.
+
+Lemma discrete_hausdorff {dsc: discrete_space T} : hausdorff_space.
+Proof.
+by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->.
+Qed.
+
+
+Lemma compact_cluster_set1 (x : T) F V :
+  hausdorff_space -> compact V -> nbhs x V ->
+  ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
+Proof.
+move=> ? cptV nxV PF FV clFx1 U nbhsU; rewrite nbhs_simpl.
+wlog oU : U nbhsU / open U.
+  rewrite /= nbhsE in nbhsU; case: nbhsU => O oO OsubU /(_ O) WH.
+  by apply: (filterS OsubU); apply: WH; [exact: open_nbhs_nbhs | by case: oO].
+have /compact_near_coveringP : compact (V `\` U).
+  apply: (subclosed_compact _ cptV) => //.
+  by apply: closedI; [exact: compact_closed | exact: open_closedC].
+move=> /(_ _ (powerset_filter_from F) (fun W x => ~ W x))[].
+  move=> z [Vz ?]; have zE : x <> z by move/nbhs_singleton: nbhsU => /[swap] ->.
+  have : ~ cluster F z by move: zE; apply: contra_not; rewrite clFx1 => ->.
+  case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /set0P/negP/negPn/eqP.
+  rewrite setIC => /disjoints_subset CD0; exists (D, [set W | F W /\ W `<=` C]).
+    by split; rewrite //= nbhs_simpl; exact: powerset_filter_fromP.
+  by case => t W [Dt] [FW] /subsetCP; apply; apply: CD0.
+move=> M [MF ME2 [W] MW /(_ _ MW) VUW].
+apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF.
+by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t).
+Qed.
+
+Lemma compact_precompact (A : set T) :
+  hausdorff_space -> compact A -> precompact A.
+Proof.
+move=> h c; rewrite precompactE ( _ : closure A = A)//.
+by apply/esym/closure_id; exact: compact_closed.
+Qed.
+
+Lemma open_hausdorff : hausdorff_space =
+  forall (x y : T), x != y ->
+    exists2 AB, (x \in AB.1 /\ y \in AB.2) &
+                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
+Proof.
+rewrite propeqE; split => [T_filterT2|T_openT2] x y.
+  have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
+  move=> /[apply] /asboolPn/existsp_asboolPn[A]; rewrite -existsNE => -[B].
+  rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
+  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].
+  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].
+move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)).
+by rewrite -set0P => /(_ _ _)/negP; apply.
+Qed.
+Lemma hausdorff_accessible : hausdorff_space -> 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.
+
+Lemma accessible_closed_set1 : accessible_space -> forall (x : T), 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; 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 => //; rewrite inE in xA.
+Qed.
+
+Lemma accessible_finite_set_closed :
+  accessible_space <-> forall A : set T, finite_set A -> closed A.
+Proof.
+split => [TT1 A fA|h x y xy].
+  rewrite -(fsbig_setU_set1 fA) fsbig_finite//=.
+  by apply: closed_bigsetU => x xA; exact: accessible_closed_set1.
+exists (~` [set y]); split; first by rewrite openC; exact: h.
+by rewrite !inE/=; split=> [|/eqP]; [exact/eqP|rewrite eqxx].
+Qed.
+
+End point_separation_axioms.
+
+Arguments hausdorff_space : clear implicits.
+Arguments accessible_space : clear implicits.
+Arguments kolmogorov_space : clear implicits.
+
+Lemma subspace_hausdorff {T : topologicalType} (A : set T) :
+  hausdorff_space T -> hausdorff_space (subspace A).
+Proof.
+rewrite ?open_hausdorff => + x y xNy => /(_ x y xNy).
+move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ].
+by move=> ?; exists (P, Q); split => //=; [exact: oP | exact: oQ].
+Qed.
+
+Lemma order_hausdorff {d} {T : orderTopologicalType d} : hausdorff_space T.
+Proof.
+rewrite open_hausdorff=> p q; wlog : p q / (p < q)%O.
+  have /orP[] := le_total p q; rewrite le_eqVlt => /predU1P[->|].
+  - by rewrite eqxx.
+  - by move=> ?; exact.
+  - by rewrite eqxx.
+  - move=> qp WH; rewrite eq_sym => /(WH _ _ qp)[[P Q] [? ?] [? ? ?]].
+    by exists (Q, P); split; rewrite // setIC.
+move=> plq ?; have [[z /andP[pz zq]]|] := pselect (exists z, p < z < q)%O.
+  exists (`]-oo,z[, `]z,+oo[)%classic.
+    by split => //=; apply/mem_set; rewrite set_itvE.
+  split => //= ; apply/eqP; rewrite -subset0 => r; rewrite set_itvE => -[/= rz].
+  by apply/negP; rewrite in_itv/= andbT -leNgt (ltW rz).
+move=> npzq; exists (`]-oo, q[, `]p, +oo[)%classic; split => //=.
+- by apply /mem_set; rewrite set_itvE.
+- by apply /mem_set; rewrite set_itvE.
+- apply/eqP; rewrite -subset0 => r; rewrite !set_itvE => -[/= rz zr].
+  by apply: npzq; exists r; rewrite rz zr.
+Qed.
+
+
+Section ball_hausdorff.
+Variables (R : numDomainType) (T : pseudoMetricType R).
+
+Lemma ball_hausdorff : hausdorff_space T =
+  forall (a b : T), a != b ->
+  exists r : {posnum R} * {posnum R},
+    ball a r.1%:num `&` ball b r.2%:num == set0.
+Proof.
+rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
+  move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]].
+  have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by apply: open_nbhs_nbhs.
+  have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by apply: open_nbhs_nbhs.
+  by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0).
+move=> r s /eqP brs_eq0; exists ((ball a r%:num)^°, (ball b s%:num)^°) => /=.
+  split; by rewrite inE; apply: nbhs_singleton; apply: nbhs_interior;
+            apply/nbhs_ballP; apply: in_filter_from => /=.
+split; do ?by apply: open_interior.
+by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset.
+Qed.
+End ball_hausdorff.
+
+Import numFieldTopology.Exports.
+Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
+Proof. exact: order_hausdorff. Qed.
+
+Section separated_topologicalType.
+Variable T : topologicalType.
+Implicit Types x y : T.
+
+Local Open Scope classical_set_scope.
+Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.
+
+Lemma closeEnbhs x : close x = cluster (nbhs x).
+Proof.
+transitivity (cluster (open_nbhs x)); last first.
+  by rewrite /cluster; under eq_fun do rewrite -meets_openl.
+rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets.
+apply/eq_forall => A; rewrite forall_swap.
+by rewrite closureEonbhs/= meets_globallyl.
+Qed.
+
+Lemma closeEonbhs x : close x = [set y | open_nbhs x `#` open_nbhs y].
+Proof.
+by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
+Qed.
+
+Lemma close_sym x y : close x y -> close y x.
+Proof. by rewrite !closeEnbhs /cluster/= meetsC. Qed.
+
+Lemma cvg_close {F} {FF : ProperFilter F} x y : F --> x -> F --> y -> close x y.
+Proof.
+by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx.
+Qed.
+
+Lemma close_refl x : close x x.
+Proof. exact: (@cvg_close (nbhs x)). Qed.
+Hint Resolve close_refl : core.
+
+Lemma cvgx_close x y : x --> y -> close x y.
+Proof. exact: cvg_close. Qed.
+
+Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
+  {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
+Proof.
+move=> f_prop fFl fFl'.
+suff f_totalfun: {near F, is_totalfun f}.
+  by apply: cvg_close fFl fFl'; exact: fmapi_proper_filter.
+apply: filter_app f_prop; near do split=> //=.
+have: (f `@ F) setT by apply: fFl; apply: filterT.
+by rewrite fmapiE; apply: filterS => x [y []]; exists y.
+Unshelve. all: by end_near. Qed.
+Definition cvg_toi_locally_close := @cvgi_close.
+
+Hypothesis sep : hausdorff_space T.
+
+Lemma closeE x y : close x y = (x = y).
+Proof.
+rewrite propeqE; split; last by move=> ->; exact: close_refl.
+by rewrite closeEnbhs; exact: sep.
+Qed.
+
+Lemma close_eq x y : close x y -> x = y.
+Proof. by rewrite closeE. Qed.
+
+
+Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
+Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
+
+Lemma cvg_eq x y : x --> y -> x = y.
+Proof. by rewrite -closeE //; apply: cvg_close. Qed.
+
+Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
+  {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
+Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
+
+
+End separated_topologicalType.
+
+Section separated_ptopologicalType.
+Variable T : ptopologicalType.
+Implicit Types x y : T.
+
+Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} :
+  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
+Proof.
+move=> F12 F21.
+have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
+  by apply: (@cvg_close _ F2) => //; apply: cvgP F2l.
+have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
+rewrite dvgP // dvgP //; exact/close_refl.
+Qed.
+
+Hypothesis sep : hausdorff_space T.
+
+Lemma lim_id x : lim (nbhs x) = x.
+Proof. by apply/esym/cvg_eq/cvg_ex => //; exists x. Qed.
+
+Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
+  f @ F --> l -> lim (f @ F) = l.
+Proof. by move=> /[dup] /cvgP /cvg_unique; apply. Qed.
+
+Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
+   (\forall x \near F, f x = l) -> lim (f @ F) = l.
+Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
+
+Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
+   lim ((fun _ : U => k) @ F) = k.
+Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
+
+Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
+  F (fun x : U => is_subset1 (f x)) ->
+  f `@ F --> l -> lim (f `@ F) = l.
+Proof.
+move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
+Qed.
+
+End separated_ptopologicalType.
+
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
+Notation cvg_map_lim := cvg_lim (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgi_lim`")]
+Notation cvgi_map_lim := cvgi_lim (only parsing).
+
+#[global] Hint Resolve close_refl : core.
+Arguments close_cvg {T} F1 F2 {FF2} _.
+
+Section close_uniform.
+Implicit Types (U : uniformType).
+Lemma entourage_close {U} (x y : U) : close x y = forall A, entourage A -> A (x, y).
+Proof.
+rewrite propeqE; split=> [cxy A entA|cxy].
+  have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy.
+  have yl := nbhs_entourage _ (entourage_inv entsA).
+  have yr := nbhs_entourage _ entsA.
+  have [z [/xsectionP zx /xsectionP zy]] := cxy _ _ (yr x) (yl y).
+  exact: (entourage_split z).
+rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B].
+exists y; split.
+- by apply/sE1A/xsectionP; exact: cxy.
+- by apply/sE2B/xsectionP; exact: entourage_refl.
+Qed.
+
+Lemma close_trans {U} (y x z : U) : close x y -> close y z -> close x z.
+Proof.
+rewrite !entourage_close => cxy cyz A entA.
+exact: entourage_split (cxy _ _) (cyz _ _).
+Qed.
+
+Lemma close_cvgxx {U} (x y : U) : close x y -> x --> y.
+Proof.
+rewrite entourage_close => cxy P /= /nbhsP[A entA sAP].
+apply/nbhsP; exists (split_ent A) => // z /xsectionP xz; apply: sAP.
+apply/xsectionP; apply: (entourage_split x) => //.
+by have := cxy _ (entourage_inv (entourage_split_ent entA)).
+Qed.
+
+
+Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
+  F --> l <-> ([cvg F in U] /\ close (lim F) l).
+Proof.
+move=> FF; split=> [Fl|[cvF]Cl].
+  by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F).
+by apply: cvg_trans (close_cvgxx Cl).
+Qed.
+
+Lemma ball_close {R : numFieldType} {M : pseudoMetricType R} (x y : M) :
+  close x y = forall eps : {posnum R}, ball x eps%:num y.
+Proof.
+rewrite propeqE; split => [cxy eps|cxy].
+  have := !! cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos).
+  rewrite closureEonbhs/= meetsC meets_globallyr.
+  move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]].
+  by apply: (@ball_splitl _ _ z); apply: interior_subset.
+rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]]
+  /nbhs_ballP[_/posnumP[e1 e1A]].
+by exists y; split; [apply/e2B|apply/e1A; exact: ballxx].
+Qed.
+End close_uniform.
+
+Section set_separations.
+Context {T : topologicalType}.
+Definition normal_space :=
+  forall A : set T, closed A ->
+    filter_from (set_nbhs A) closure `=>` set_nbhs A.
+
+Definition regular_space :=
+  forall a : T, filter_from (nbhs a) closure --> a.
+
+Lemma compact_regular (x : T) V : hausdorff_space T -> compact V -> 
+  nbhs x V -> {for x, regular_space}.
+Proof.
+move=> sep cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //.
+- apply: filter_from_proper => //; first last.
+    by move=> ? /nbhs_singleton/subset_closure ?; exists x.
+  apply: filter_from_filter; first by exists setT; exact: filterT.
+  move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI].
+- by exists V => //; have /closure_id <- : closed V by exact: compact_closed.
+rewrite eqEsubset; split; first last.
+  move=> _ -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //.
+  by apply/CA/subset_closure; exact: nbhs_singleton.
+move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply].
+move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0].
+apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP.
+split; first by exists A => //; exact: open_nbhs_nbhs.
+apply/not_implyP; split; first exact: open_nbhs_nbhs.
+apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset.
+have /closure_id -> : closed (~` B); first by exact: open_closedC.
+by apply/closure_subset/disjoints_subset; rewrite setIC.
+Qed.
+
+End set_separations.
+
+Arguments normal_space : clear implicits.
+Arguments regular_space : clear implicits.
+
+Local Open Scope relation_scope.
+Lemma uniform_regular {T : uniformType} : @regular_space T.
+Proof.
+move=> x R /=; rewrite -{1}nbhs_entourageE => -[E entE ER].
+pose E' := split_ent E; have eE' : entourage E' by exact: entourage_split_ent.
+exists (xsection (E' `&` E'^-1) x).
+  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
+  exact: filterI.
+move=> z /= clEz; apply/ER/xsectionP; apply: subset_split_ent => //.
+have [] := clEz (xsection (E' `&` E'^-1) z).
+  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
+  exact: filterI.
+by move=> y /= [/xsectionP[? ?] /xsectionP[? ?]]; exists y.
+Qed.
+Local Close Scope relation_scope.
+
+#[global] Hint Resolve uniform_regular : core.
+
+
+
+Section totally_disconnected.
+Implicit Types T : topologicalType.
+
+Definition totally_disconnected {T} (A : set T) :=
+  forall x, A x -> connected_component A x = [set x].
+
+Definition zero_dimensional T :=
+  (forall x y, x != y -> exists U : set T, [/\ clopen U, U x & ~ U y]).
+
+Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T.
+Proof.
+move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP.
+by split; [exact: discrete_open | exact: discrete_closed].
+Qed.
+
+Lemma zero_dimension_totally_disconnected {T} :
+  zero_dimensional T -> totally_disconnected [set: T].
+Proof.
+move=> zdA x _; rewrite eqEsubset.
+split=> [z [R [Rx _ ctdR Rz]]|_ ->]; last exact: connected_component_refl.
+apply: contrapT => /eqP znx; have [U [[oU cU] Uz Ux]] := zdA _ _  znx.
+suff : R `&` U = R by move: Rx => /[swap] <- [].
+by apply: ctdR; [exists z|exists U|exists U].
+Qed.
+
+Lemma zero_dimensional_cvg {T} (x : T) :
+  hausdorff_space T -> zero_dimensional T -> compact [set: T] ->
+  filter_from [set D : set T | D x /\ clopen D] id --> x.
+Proof.
+pose F := filter_from [set D : set T | D x /\ clopen D] id.
+have FF : Filter F.
+  apply: filter_from_filter; first by exists setT; split => //; exact: clopenT.
+  by move=> A B [? ?] [? ?]; exists (A `&` B) => //; split=> //; exact: clopenI.
+have PF : ProperFilter F by apply: filter_from_proper; move=> ? [? _]; exists x.
+move=> hsdfT zdT cmpT U Ux; rewrite nbhs_simpl -/F.
+wlog oU : U Ux / open U.
+  move: Ux; rewrite /= nbhsE => -[] V [? ?] /filterS + /(_ V) P.
+  by apply; apply: P => //; exists V.
+have /(iffLR (compact_near_coveringP _)) : compact (~` U).
+  by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC.
+move=> /(_ _ _ setC (powerset_filter_from_filter PF))[].
+  move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y.
+    by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton.
+  exists (~` C, [set U | U `<=` C]); first split.
+  - by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
+  - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans.
+    by exists C => //; exists C.
+  - by case=> i j [? /subsetC]; apply.
+by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF.
+Qed.
+
+Lemma zero_dimensional_ray {d} {T : orderTopologicalType d} (x y : T) : 
+  (x < y)%O -> zero_dimensional T ->
+  exists U, [/\ clopen U, U y , ~ U x & forall l r, U r -> ~ U l -> l < r]%O.
+Proof.
+move=> xy zt; have xNy : y != x by move: xy; rewrite lt_def => /andP[].
+have [U [clU Uy nUx]] := zt y x xNy.
+have := clopen_bigcup_clopen clU Uy; set I := (I in clopen I); case=> ? ?.
+pose V := I `|` `[y, +oo[; have Iy : I y.
+  case: clU => + _; rewrite openE => /(_ _ Uy).
+  rewrite /interior /= itv_nbhsE /= => -[i [] iy yi iU].
+  by exists i => //; split => //; exact: itv_open_ends_open.
+have IU : I `<=` U by move=> ? [? [+ _ _]] => /subset_trans; exact.
+exists V; split; first split.
+- suff -> : V = I `|` `]y,+oo[ by exact: openU.
+  rewrite eqEsubset; split => z; case; first by left.
+  + by rewrite -setU1itv // => -[->|]; [left| right].
+  + by left.
+  + by rewrite /V -setU1itv //; right; right.
+- by apply: closedU => //; exact: rray_closed.
+- by left.
+- by move=> [/IU //|]; rewrite set_itvE/= leNgt xy.
+- move=> l r Vr Vl; rewrite ltNge; apply/negP; move: Vl; apply: contra_not.
+  move=> rl; case: Vr; first last.
+    by rewrite set_itvE => yr; right; rewrite set_itvE; exact: (le_trans yr).
+  have /orP[|ly] := le_total y l; first by move=> + _; right; rewrite set_itvE.
+  case=> i [iu oi /= yi ri]; left; exists i; first by split.
+  move: iu oi => _ _; case: i yi ri => p q /= /andP [py yq] /andP[pr rq].
+  apply/andP; split.
+  + by rewrite (le_trans pr)// bnd_simp.
+  + by rewrite (le_trans _ yq)// bnd_simp.
+Qed.
+
+End totally_disconnected.
+(* This section proves that uniform spaces, with a countable base for their
+   entourage, are metrizable. The definition of this metric is rather arcane,
+   and the proof is tough. That's ok because the resulting metric is not
+   intended to be used explicitly. Instead, this is typically used in
+   applications that do not depend on the metric:
+   - `metric spaces are T4`
+   - `in metric spaces, compactness and sequential compactness agree`
+   - infinite products of metric spaces are metrizable
+*)
+Module countable_uniform.
+Section countable_uniform.
+Local Open Scope relation_scope.
+Context {R : realType} {T : uniformType}.
+
+Hypothesis cnt_unif : @countable_uniformity T.
+
+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 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.
+
+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`
+   - each (g_ n) is symmetric
+   - the sets (g_ n) are nested downward
+   - g_ n.+1 \o g_ n.+1 \o g_ n.+1 `<=` g_ n says the sets descend `quickly`
+ *)
+
+Local Fixpoint g_ n : set (T * T) :=
+  if n is n.+1 then let W := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1
+  else [set: T*T].
+
+Let entG n : entourage (g_ n).
+Proof.
+elim: n => /=; first exact: entourageT.
+by move=> n entg; apply/entourage_invI; exact: filterI.
+Qed.
+
+Local Lemma symG n : (g_ n)^-1 = g_ n.
+Proof.
+by case: n => // n; rewrite eqEsubset; split; case=> ? ?; rewrite /= andC.
+Qed.
+
+Local Lemma descendG1 n : g_ n.+1 `<=` g_ n.
+Proof.
+apply: subIset; left; apply: subIset; left; apply: subset_trans.
+  by apply: split_ent_subset; exact: entourage_split_ent.
+by apply: subset_trans; last exact: split_ent_subset.
+Qed.
+
+Local Lemma descendG n m : (m <= n)%N -> g_ n `<=` g_ m.
+Proof.
+elim: n; rewrite ?leqn0; first by move=>/eqP ->.
+move=> n IH; rewrite leq_eqVlt ltnS => /orP [/eqP <- //|] /IH.
+by apply: subset_trans; exact: descendG1.
+Qed.
+
+Local Lemma splitG3 n : g_ n.+1 \; g_ n.+1 \; g_ n.+1 `<=` g_ n.
+Proof.
+suff g2split : g_ n.+1 \; g_ n.+1 `<=` split_ent (g_ n).
+  apply: subset_trans; last exact: subset_split_ent (entG n).
+  apply: set_compose_subset (g2split); rewrite -[_ n.+1]set_compose_diag.
+  apply: subset_trans g2split; apply: set_compose_subset => //.
+  by move=> [_ _] [z _] [<- <-]; exact: entourage_refl.
+apply: subset_trans; last exact: subset_split_ent.
+by apply: set_compose_subset; apply: subIset; left; apply: subIset; left.
+Qed.
+
+Local Lemma gsubf n : g_ n.+1 `<=` f_ n.
+Proof. by apply: subIset; left; apply: subIset; right. Qed.
+
+Local Lemma countableBaseG A : entourage A -> exists N, g_ N `<=` A.
+Proof.
+move=> /countableBase [N] fnA; exists N.+1.
+by apply: subset_trans fnA; exact: gsubf.
+Qed.
+
+(* Step 2.
+   We build a sensible notion of balls for our metric.
+   The naive attempt,
+                     `ball x e y := g_ (distN e) (x,y))
+   doesn't respect triangle inequality. We need to cook triangle inequality
+   into the balls themselves. So we define balls in terms of steps:
+      `ball x e y := there are n steps x_0 = x,...,x_i,..., x_n.+1 = y and
+                     e_1,...,e_n such that
+                           g_ (distN e_i) (x_i,x_i+1)
+                                    and
+                               sum (e_i) = e
+*)
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Local Definition distN (e : R) : nat := `|Num.floor e^-1|%N.
+
+Local Lemma distN0 : distN 0 = 0%N.
+Proof. by rewrite /distN invr0 floor0. Qed.
+
+Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n.
+Proof.
+rewrite /distN invrK.
+apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm ?floor_ge0//.
+by rewrite -intrEfloor intrEge0.
+Qed.
+
+Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.
+Proof.
+move=> e1pos e1e2; rewrite /distN; apply: lez_abs2.
+  by rewrite floor_ge0 ltW// invr_gt0 (lt_le_trans _ e1e2).
+by rewrite floor_le// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2).
+Qed.
+
+Local Fixpoint n_step_ball n x e z :=
+  if n is n.+1 then exists y d1 d2,
+    [/\ n_step_ball n x d1 y,
+        0 < d1,
+        0 < d2,
+        g_ (distN d2) (y, z) &
+        d1 + d2 = e]
+  else e > 0 /\ g_ (distN e) (x, z).
+
+Local Definition step_ball x e z := exists i, (n_step_ball i x e z).
+
+Local Lemma n_step_ball_pos n x e z : n_step_ball n x e z -> 0 < e.
+Proof.
+by case: n => [[]|] // n; case=> [?] [?] [?] [] ? ? ? ? <-; apply: addr_gt0.
+Qed.
+
+Local Lemma step_ball_pos x e z : step_ball x e z -> 0 < e.
+Proof. by case => ?; exact: n_step_ball_pos. Qed.
+
+Local Lemma entourage_nball e :
+  0 < e -> entourage [set xy | step_ball xy.1 e xy.2].
+Proof.
+move=> epos; apply: (@filterS _ _ _ (g_ (distN e))) => // [[x y]] ?.
+by exists 0%N.
+Qed.
+
+Local Lemma n_step_ball_center x e : 0 < e -> n_step_ball 0 x e x.
+Proof. by move=> epos; split => //; exact: entourage_refl. Qed.
+
+Local Lemma step_ball_center x e : 0 < e -> step_ball x e x.
+Proof. by move=> epos; exists 0%N; apply: n_step_ball_center. Qed.
+
+Local Lemma n_step_ball_triangle n m x y z d1 d2 :
+  n_step_ball n x d1 y ->
+  n_step_ball m y d2 z ->
+  n_step_ball (n + m).+1 x (d1 + d2) z.
+Proof.
+move: n z d2; elim: m => [n z d2 Nxy [? ?]|n IH m z d2 Oxy].
+  by exists y, d1, d2; split; rewrite ?addn0 // (n_step_ball_pos Nxy).
+move=> [w] [e1] [e2] [Oyw ? ? ? <-].
+exists w, (d1 + e1), e2; rewrite addnS addrA.
+split => //; last by rewrite addr_gt0//; exact: n_step_ball_pos Oxy.
+by case: (IH m w e1 Oxy Oyw) => t [e3] [e4] [] Oxt ? ? ? <-; exists t, e3, e4.
+Qed.
+
+Local Lemma step_ball_triangle x y z d1 d2 :
+  step_ball x d1 y -> step_ball y d2 z -> step_ball x (d1 + d2) z.
+Proof.
+move=> [n Oxy] [m Oyz]; exists (n + m).+1.
+exact: n_step_ball_triangle Oxy Oyz.
+Qed.
+
+Local Lemma n_step_ball_sym n x y e :
+  n_step_ball n x e y -> n_step_ball n y e x.
+Proof.
+move: x y e; elim: n; first by move=> ? ? ?; rewrite /= -{1}symG.
+move=> n IH x y e [t] [d1] [d2] [] /IH Oty ? ?.
+rewrite addrC -symG -[n]add0n => gty <-; apply: (n_step_ball_triangle _ Oty).
+by split => //; exact: gty.
+Qed.
+
+Local Lemma step_ball_sym x y e : step_ball x e y -> step_ball y e x.
+Proof. by case=> n /n_step_ball_sym ?; exists n. Qed.
+
+(* Step 3:
+   We prove that step_ball respects the original entourage. This requires an
+   induction on the length of the steps, which is pretty tricky. The central
+   lemma is `split_n_step_ball`, which lets us break a list into parts three
+   parts as: half + one_step + half. Then our we can break apart our n +1 path
+
+                         nlong + one_step
+   into
+                  (half + one_step + half) + one_step
+                                =
+                  half + one_step + (half + one_step)
+
+   and we can we can use our (strong) induction hypothesis.
+   And lastly we finish with splitG3.
+*)
+
+Local Lemma n_step_ball_le n x e1 e2 :
+  e1 <= e2 -> n_step_ball n x e1 `<=` n_step_ball n x e2.
+Proof.
+move: x e1 e2; elim: n.
+  move=> x e1 e2 e1e2 y [?] gxy; split; first exact: (lt_le_trans _ e1e2).
+  by apply: descendG; last (exact: gxy); exact: distN_le.
+move=> n IH x e1 e2 e1e2 z [y] [d1] [d2] [] /IH P d1pos d2pos gyz d1d2e1.
+have d1e1d2 : d1 = e1 - d2 by rewrite -d1d2e1 -addrA subrr addr0.
+have e2d2le : e1 - d2 <= e2 - d2 by exact: lerB.
+exists y, (e2 - d2), d2; split => //.
+- by apply: P; apply: le_trans e2d2le; rewrite d1e1d2.
+- by apply: lt_le_trans e2d2le; rewrite -d1e1d2.
+- by rewrite -addrA [-_ + _]addrC subrr addr0.
+Qed.
+
+Local Lemma step_ball_le x e1 e2 :
+  e1 <= e2 -> step_ball x e1 `<=` step_ball x e2.
+Proof. by move=> e1e2 ? [n P]; exists n; exact: (n_step_ball_le e1e2). Qed.
+
+Local Lemma distN_half (n : nat) : n.+1%:R^-1 / (2:R) <= n.+2%:R^-1.
+Proof.
+rewrite -invrM //; [|exact: unitf_gt0 |exact: unitf_gt0].
+rewrite lef_pV2 ?posrE // -?natrM ?ler_nat -addn1 -addn1 -addnA mulnDr.
+by rewrite muln1 leq_add2r leq_pmull.
+Qed.
+
+Local Lemma split_n_step_ball n x e1 e2 z :
+  0 < e1 -> 0 < e2 -> n_step_ball n.+1 x (e1 + e2) z ->
+    exists t1 t2 a b,
+    [/\
+      n_step_ball a x e1 t1,
+      n_step_ball 0 t1 (e1 + e2) t2,
+      n_step_ball b t2 e2 z &
+      (a + b = n)%N
+    ].
+Proof.
+move: e1 e2 x z; elim: n.
+  move=> e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Oxy ? ? gd2yz deE.
+  case: (pselect (e1 <= d1)).
+    move=> e1d1; exists x, y, 0%N, 0%N; split.
+    - exact: n_step_ball_center.
+    - apply: n_step_ball_le; last exact: Oxy.
+      by rewrite -deE lerDl; apply: ltW.
+    - apply: (@n_step_ball_le _ _ d2); last by split.
+      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK [leLHS]addrC.
+      by rewrite [e2 + _]addrC -deE; exact: lerD.
+    - by rewrite addn0.
+  move=> /negP; rewrite -ltNge//.
+  move=> e1d1; exists y, z, 0%N, 0%N; split.
+  - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW.
+  - rewrite -deE; apply: (@n_step_ball_le _ _ d2) => //.
+    by rewrite lerDr; apply: ltW.
+  - exact: n_step_ball_center.
+  - by rewrite addn0.
+move=> n IH e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Od1xy d1pos d2pos gd2yz deE.
+case: (pselect (e2 <= d2)).
+  move=> e2d2; exists y, z, n.+1, 0%N; split.
+  - apply: (@n_step_ball_le _ _ d1); rewrite // -[e1]addr0 -(subrr e2) addrA.
+    by rewrite -deE -lerBlDr opprK lerD.
+  - apply: (@n_step_ball_le _ _ d2); last by split.
+    by rewrite -deE lerDr; exact: ltW.
+  - exact: n_step_ball_center.
+  - by rewrite addn0.
+have d1E' : d1 = e1 + (e2 - d2).
+  by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0.
+move=> /negP; rewrite -ltNge// => d2lee2.
+  case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
+  move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
+  exists t1, t2, c1, c2.+1; split => //.
+  - by apply: (@n_step_ball_le _ _ d1); rewrite -?deE // ?lerDl; exact: ltW.
+  - exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0//.
+    by rewrite -addrA [-_ + _]addrC subrr addr0.
+  - by rewrite addnS.
+Qed.
+
+Local Lemma n_step_ball_le_g x n :
+  n_step_ball 0 x n%:R^-1 `<=` [set y | g_ n (x,y)].
+Proof. by move=> y [] ?; rewrite distN_nat. Qed.
+
+Local Lemma subset_n_step_ball n x N :
+  n_step_ball n x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
+Proof.
+move: N x; elim: n {-2}n (leqnn n) => n.
+  rewrite leqn0 => /eqP -> N x; apply: subset_trans.
+    exact: n_step_ball_le_g.
+  by move=> y ?; exact: descendG.
+move=> IH1 + + N x1 x4; case.
+  by move=> ? [?] P; apply: descendG _ P; rewrite distN_nat.
+move=> l ln1 Ox1x4.
+case: (@split_n_step_ball l x1 (N.+1%:R^-1/2) (N.+1%:R^-1/2) x4) => //.
+  by rewrite -splitr.
+move=> x2 [x3] [l1] [l2] [] P1 [? +] P3 l1l2; rewrite -splitr distN_nat => ?.
+have l1n : (l1 <= n)%N by rewrite (leq_trans (leq_addr l2 l1))// l1l2 -ltnS.
+have l2n : (l2 <= n)%N by rewrite (leq_trans (leq_addl l1 l2))// l1l2 -ltnS.
+apply: splitG3; exists x3; [exists x2 => //|].
+  by move/(n_step_ball_le (distN_half N))/(IH1 _ l1n) : P1.
+by move/(n_step_ball_le (distN_half N))/(IH1 _ l2n) : P3.
+Qed.
+
+Local Lemma subset_step_ball x N :
+  step_ball x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
+Proof. by move=> y [] n; exact: subset_n_step_ball. Qed.
+
+Local Lemma step_ball_entourage : entourage = entourage_ step_ball.
+Proof.
+rewrite predeqE => E; split; first last.
+  by case=> e /= epos esubE; apply: (filterS esubE); exact: entourage_nball.
+move=> entE; case: (countableBase entE) => N fN.
+exists N.+2%:R^-1; first by rewrite /= invr_gt0.
+apply: (subset_trans _ fN); apply: subset_trans; last apply: gsubf.
+by case=> x y /= N1ball; apply: (@subset_step_ball x N.+1).
+Qed.
+
+Definition type : Type := let _ := countableBase in let _ := entF in T.
+
+#[export] HB.instance Definition _ := Uniform.on type.
+#[export] HB.instance Definition _ := Uniform_isPseudoMetric.Build R type
+  step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.
+#[export] HB.instance Definition _ {q : Pointed T} := Pointed.copy type (Pointed.Pack q).
+
+Lemma countable_uniform_bounded (x y : T) :
+  let U := [the pseudoMetricType R of type]
+  in @ball _ U x 2 y.
+Proof.
+rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
+rewrite [X in `|X|%N](_ : _ = 0) ?absz0//.
+apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt.
+by apply/andP; split => //; rewrite invf_lt1 //= ltrDl.
+Qed.
+
+End countable_uniform.
+
+
+Module Exports. HB.reexport. End Exports.
+End countable_uniform.
+Export countable_uniform.Exports.
+
+Notation countable_uniform := countable_uniform.type.
+
+Definition sup_pseudometric (R : realType) (T : Type) (Ii : Type)
+  (Tc : Ii -> PseudoMetric R T) (Icnt : countable [set: Ii]) : Type := T.
+
+Section sup_pseudometric.
+Variable (R : realType) (T : choiceType) (Ii : Type).
+Variable (Tc : Ii -> PseudoMetric R T).
+
+Hypothesis Icnt : countable [set: Ii].
+
+Local Notation S := (sup_pseudometric Tc Icnt).
+
+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)).
+
+HB.instance Definition _ : PseudoMetric R S :=
+  PseudoMetric.on (countable_uniform countable_uniformityT).
+
+End sup_pseudometric.
+
+
+Module gauge.
+Section gauge.
+Local Open Scope relation_scope.
+
+Let split_sym {T : uniformType} (W : set (T * T)) :=
+  (split_ent W) `&` (split_ent W)^-1.
+
+Section entourage_gauge.
+Context {T : uniformType} (E : set (T * T)) (entE : entourage E).
+
+Definition gauge :=
+  filter_from [set: nat] (fun n => iter n split_sym (E `&` E^-1)).
+
+Lemma iter_split_ent j : entourage (iter j split_sym (E `&` E^-1)).
+Proof. by elim: j => [|i IH]; exact: filterI. Qed.
+
+Lemma gauge_ent A : gauge A -> entourage A.
+Proof.
+case=> n; elim: n A; first by move=> ? _ /filterS; apply; apply: filterI.
+by move=> n ? A _ /filterS; apply; apply: filterI; have ? := iter_split_ent n.
+Qed.
+
+Lemma gauge_filter : Filter gauge.
+Proof.
+apply: filter_from_filter; first by exists 0%N.
+move=> i j _ _; wlog ilej : i j / (i <= j)%N.
+  by move=> WH; have [|/ltnW] := leqP i j;
+    [|rewrite (setIC (iter _ _ _))]; exact: WH.
+exists j => //; rewrite subsetI; split => //; elim: j i ilej => [i|j IH i].
+  by rewrite leqn0 => /eqP ->.
+rewrite leq_eqVlt => /predU1P[<-//|/ltnSE/IH]; apply: subset_trans.
+by move=> x/= [jx _]; apply: split_ent_subset => //; exact: iter_split_ent.
+Qed.
+
+Lemma gauge_refl A : gauge A -> diagonal `<=` A.
+Proof.
+case=> n _; apply: subset_trans => -[_ a]/diagonalP ->.
+by apply: entourage_refl; exact: iter_split_ent.
+Qed.
+
+Lemma gauge_inv A : gauge A -> gauge A^-1.
+Proof.
+case=> n _ EA; apply: (@filterS _ _ _ (iter n split_sym (E `&` E^-1))).
+- exact: gauge_filter.
+- by case: n EA; last move=> n; move=> EA [? ?] [/=] ? ?; exact: EA.
+- by exists n .
+Qed.
+
+Lemma gauge_split A : gauge A -> exists2 B, gauge B & B \; B `<=` A.
+Proof.
+case => n _ EA; exists (iter n.+1 split_sym (E `&` E^-1)); first by exists n.+1.
+apply: subset_trans EA; apply: subset_trans; first last.
+  by apply: subset_split_ent; exact: iter_split_ent.
+by case=> a c [b] [] ? ? [] ? ?; exists b.
+Qed.
+
+Let gauged : Type := T.
+
+HB.instance Definition _ := Choice.on gauged.
+HB.instance Definition _ :=
+  @isUniform.Build gauged gauge gauge_filter gauge_refl gauge_inv gauge_split.
+
+Lemma gauge_countable_uniformity : countable_uniformity gauged.
+Proof.
+exists [set iter n split_sym (E `&` E^-1) | n in [set: nat]].
+split; [exact: card_image_le | by move=> W [n] _ <-; exists n|].
+by move=> D [n _ ?]; exists (iter n split_sym (E `&` E^-1)).
+Qed.
+
+Definition type := countable_uniform.type gauge_countable_uniformity.
+End entourage_gauge.
+
+End gauge.
+Module Exports. HB.reexport. End Exports.
+End gauge.
+Export gauge.Exports.
+
+Lemma uniform_pseudometric_sup {R : realType} {T : puniformType} :
+    @entourage T = @sup_ent T {E : set (T * T) | @entourage T E}
+  (fun E => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).
+Proof.
+rewrite eqEsubset; split => [E entE|E].
+  exists E => //=.
+  pose pe : {classic {E0 : set (T * T) | _}} * _ := (exist _ E entE, E).
+  have entPE : `[< @entourage (gauge.type entE) E >].
+    by apply/asboolP; exists 0%N => // ? [].
+  exists (fset1 (exist _ pe entPE)) => //=; first by move=> ?; rewrite in_setE.
+  by rewrite set_fset1 bigcap_set1.
+case=> W /= [/= J] _ <- /filterS; apply; apply: filter_bigI => -[] [] [] /= D.
+move=> entD G /[dup] /asboolP [n _ + _ _] => /filterS; apply.
+exact: gauge.iter_split_ent.
+Qed.
+
+Section perfect_sets.
+
+Implicit Types (T : topologicalType).
+
+Definition perfect_set {T} (A : set T) := closed A /\ limit_point A = A.
+
+Lemma perfectTP {T} : perfect_set [set: T] <-> forall x : T, ~ open [set x].
+Proof.
+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.
+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.
+  by split => // ? ->.
+by exists y; split => //; [exact/eqP | exact: VU].
+Qed.
+
+Lemma perfect_set2 {T} : perfect_set [set: T] <->
+  forall (U : set T), open U -> U !=set0 ->
+  exists x y, [/\ U x, U y & x != y] .
+Proof.
+apply: iff_trans; first exact: perfectTP; split.
+  move=> nx1 U oU [] x Ux; exists x.
+  have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1.
+  apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset.
+  (split => //; last by move=> ? ->); move=> y Uy; have  /not_and3P := Uyx y.
+  by case => // /negP; rewrite negbK => /eqP ->.
+move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
+by move=> y [] ? [->] -> /eqP.
+Qed.
+
+End perfect_sets.
\ No newline at end of file
diff --git a/theories/topology.v b/theories/topology.v
index c94d964a7..9ee494677 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -86,7 +86,6 @@ From mathcomp Require Export filter.
 (*                        cluster F == set of cluster points of F             *)
 (*                          compact == set of compact sets w.r.t. the filter- *)
 (*                                     based definition of compactness        *)
-(*               hausdorff_space T <-> T is a Hausdorff space (T2)            *)
 (*                   compact_near F == the filter F contains a closed compact *)
 (*                                     set                                    *)
 (*                     precompact A == the set A is contained in a closed and *)
@@ -103,20 +102,10 @@ From mathcomp Require Export filter.
 (*                    near_covering == a reformulation of covering compact    *)
 (*                                     better suited for use with `near`      *)
 (*             near_covering_within == equivalent definition of near_covering *)
-(*              kolmogorov_space T <-> T is a Kolmogorov space (T0)           *)
-(*              accessible_space T <-> T is an accessible space (T1)          *)
-(*                       close x y <-> x and y are arbitrarily close w.r.t.   *)
-(*                                     to balls                               *)
 (*                     connected A <-> the only non empty subset of A which   *)
 (*                                     is both open and closed in A is A      *)
 (*                    separated A B == the two sets A and B are separated     *)
 (*            connected_component x == the connected component of point x     *)
-(*                    perfect_set A == A is closed, and every point in A is   *)
-(*                                     a limit point of A                     *)
-(*           totally_disconnected A == the only connected subsets of A are    *)
-(*                                     empty or singletons                    *)
-(*               zero_dimensional T == points are separable by a clopen set   *)
-(*                       set_nbhs A == filter from open sets containing A     *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ### Uniform spaces                                                         *)
@@ -221,13 +210,6 @@ From mathcomp Require Export filter.
 (*                            When the family f separates points from closed  *)
 (*                            sets, join_product is an embedding.             *)
 (*            singletons T := [set [set x] | x in [set: T]]                   *)
-(*                 gauge E == for an entourage E, gauge E is a filter which   *)
-(*                            includes `iter n split_ent E`                   *)
-(*                            Critically, `gauge E` forms a uniform space     *)
-(*                            with a countable uniformity.                    *)
-(*                            gauge.type is endowed with a pseudoMetricType   *)
-(*          normal_space X == X is normal (sometimes called T4)               *)
-(*         regular_space X == X is regular (sometimes called T3)              *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -1381,7 +1363,6 @@ have [|p [Bp Fp]] := Bco F; first exact: filterS FA.
 by exists p; split=> //; apply: Acl=> C Cp; apply: Fp.
 Qed.
 
-Definition hausdorff_space := forall p q : T, cluster (nbhs p) q -> p = q.
 
 Typeclasses Opaque within.
 Global Instance within_nbhs_proper (A : set T) p :
@@ -1391,13 +1372,6 @@ move=> clAp; apply: Build_ProperFilter_ex => B.
 by move=> /clAp [q [Aq AqsoBq]]; exists q; apply: AqsoBq.
 Qed.
 
-Lemma compact_closed (A : set T) : hausdorff_space -> compact A -> closed A.
-Proof.
-move=> hT Aco p clAp; have pA := !! @withinT _ (nbhs p) A _.
-have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //.
-by apply: cvg_cluster clsAp_q; apply: cvg_within.
-Qed.
-
 Lemma compact_set1 (x : T) : compact [set x].
 Proof.
 move=> F PF Fx; exists x; split; first by [].
@@ -1416,8 +1390,6 @@ by rewrite closure_id => /[dup] + <- => <- /(_ FB) Bx; exists x.
 Qed.
 End Compact.
 
-Arguments hausdorff_space : clear implicits.
-
 Section ClopenSets.
 Implicit Type T : topologicalType.
 
@@ -1552,29 +1524,6 @@ rewrite /= -[_ --> p]/([set _ | _] p) -ultra_cvg_clusterE.
 by move=> /(cvg_cluster sFG); exists p.
 Qed.
 
-Lemma compact_cluster_set1 {T : topologicalType} (x : T) F V :
-  hausdorff_space T -> compact V -> nbhs x V ->
-  ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
-Proof.
-move=> ? cptV nxV PF FV clFx1 U nbhsU; rewrite nbhs_simpl.
-wlog oU : U nbhsU / open U.
-  rewrite /= nbhsE in nbhsU; case: nbhsU => O oO OsubU /(_ O) WH.
-  by apply: (filterS OsubU); apply: WH; [exact: open_nbhs_nbhs | by case: oO].
-have /compact_near_coveringP : compact (V `\` U).
-  apply: (subclosed_compact _ cptV) => //.
-  by apply: closedI; [exact: compact_closed | exact: open_closedC].
-move=> /(_ _ (powerset_filter_from F) (fun W x => ~ W x))[].
-  move=> z [Vz ?]; have zE : x <> z by move/nbhs_singleton: nbhsU => /[swap] ->.
-  have : ~ cluster F z by move: zE; apply: contra_not; rewrite clFx1 => ->.
-  case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /set0P/negP/negPn/eqP.
-  rewrite setIC => /disjoints_subset CD0; exists (D, [set W | F W /\ W `<=` C]).
-    by split; rewrite //= nbhs_simpl; exact: powerset_filter_fromP.
-  by case => t W [Dt] [FW] /subsetCP; apply; apply: CD0.
-move=> M [MF ME2 [W] MW /(_ _ MW) VUW].
-apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF.
-by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t).
-Qed.
-
 Section Precompact.
 
 Context {X : topologicalType}.
@@ -1615,13 +1564,6 @@ Proof.
 by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB.
 Qed.
 
-Lemma compact_precompact (A : set X) :
-  hausdorff_space X -> compact A -> precompact A.
-Proof.
-move=> h c; rewrite precompactE ( _ : closure A = A)//.
-by apply/esym/closure_id; exact: compact_closed.
-Qed.
-
 Lemma precompact_closed (A : set X) : closed A -> precompact A = compact A.
 Proof.
 move=> clA; rewrite propeqE; split=> [[B AsubB [ + _ ]]|].
@@ -1780,244 +1722,6 @@ move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //.
 by rewrite set_imfset /=; exists y.
 Qed.
 
-Section set_nbhs.
-Context {T : topologicalType} (A : set T).
-
-Definition set_nbhs := \bigcap_(x in A) nbhs x.
-
-Global Instance set_nbhs_filter : Filter set_nbhs.
-Proof.
-split => P Q; first by exact: filterT.
-  by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx].
-by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact.
-Qed.
-
-Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs.
-Proof.
-case=> x Ax; split; last exact: set_nbhs_filter.
-by move/(_ x Ax)/nbhs_singleton.
-Qed.
-
-Lemma set_nbhsP (B : set T) :
-   set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]).
-Proof.
-split; first last.
-  by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs.
-move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B].
-  have [/snB|?] := pselect (A x); last by exists point.
-  by rewrite nbhsE => -[V [? ? ?]]; exists V.
-exists (\bigcup_(x in A) (projT1 (cid (Ux x)))); split.
-- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)).
-- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)).
-- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact.
-Qed.
-
-End set_nbhs.
-
-Section separated_topologicalType.
-Variable T : topologicalType.
-Implicit Types x y : T.
-
-Local Open Scope classical_set_scope.
-
-Definition kolmogorov_space := forall x y, x != y ->
-  exists A : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).
-
-Definition accessible_space := forall x y, x != y ->
-  exists A : set T, open A /\ x \in A /\ y \in ~` A.
-
-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; 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 => //; rewrite inE in xA.
-Qed.
-
-Lemma accessible_finite_set_closed :
-  accessible_space <-> forall A : set T, finite_set A -> closed A.
-Proof.
-split => [TT1 A fA|h x y xy].
-  rewrite -(fsbig_setU_set1 fA) fsbig_finite//=.
-  by apply: closed_bigsetU => x xA; exact: accessible_closed_set1.
-exists (~` [set y]); split; first by rewrite openC; exact: h.
-by rewrite !inE/=; split=> [|/eqP]; [exact/eqP|rewrite eqxx].
-Qed.
-
-Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.
-
-Lemma closeEnbhs x : close x = cluster (nbhs x).
-Proof.
-transitivity (cluster (open_nbhs x)); last first.
-  by rewrite /cluster; under eq_fun do rewrite -meets_openl.
-rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets.
-apply/eq_forall => A; rewrite forall_swap.
-by rewrite closureEonbhs/= meets_globallyl.
-Qed.
-
-Lemma closeEonbhs x : close x = [set y | open_nbhs x `#` open_nbhs y].
-Proof.
-by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
-Qed.
-
-Lemma close_sym x y : close x y -> close y x.
-Proof. by rewrite !closeEnbhs /cluster/= meetsC. Qed.
-
-Lemma cvg_close {F} {FF : ProperFilter F} x y : F --> x -> F --> y -> close x y.
-Proof.
-by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx.
-Qed.
-
-Lemma close_refl x : close x x.
-Proof. exact: (@cvg_close (nbhs x)). Qed.
-Hint Resolve close_refl : core.
-
-Lemma cvgx_close x y : x --> y -> close x y.
-Proof. exact: cvg_close. Qed.
-
-Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
-  {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
-Proof.
-move=> f_prop fFl fFl'.
-suff f_totalfun: {near F, is_totalfun f}.
-  by apply: cvg_close fFl fFl'; exact: fmapi_proper_filter.
-apply: filter_app f_prop; near do split=> //=.
-have: (f `@ F) setT by apply: fFl; apply: filterT.
-by rewrite fmapiE; apply: filterS => x [y []]; exists y.
-Unshelve. all: by end_near. Qed.
-Definition cvg_toi_locally_close := @cvgi_close.
-
-Lemma open_hausdorff : hausdorff_space T =
-  forall x y, x != y ->
-    exists2 AB, (x \in AB.1 /\ y \in AB.2) &
-                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
-Proof.
-rewrite propeqE; split => [T_filterT2|T_openT2] x y.
-  have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
-  move=> /[apply] /asboolPn/existsp_asboolPn[A]; rewrite -existsNE => -[B].
-  rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
-  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].
-  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].
-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.
-
-Definition normal_space :=
-  forall A : set T, closed A ->
-    filter_from (set_nbhs A) closure `=>` set_nbhs A.
-
-Definition regular_space :=
-  forall a : T, filter_from (nbhs a) closure --> a.
-
-Hypothesis sep : hausdorff_space T.
-
-Lemma closeE x y : close x y = (x = y).
-Proof.
-rewrite propeqE; split; last by move=> ->; exact: close_refl.
-by rewrite closeEnbhs; exact: sep.
-Qed.
-
-Lemma close_eq x y : close x y -> x = y.
-Proof. by rewrite closeE. Qed.
-
-
-Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
-Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
-
-Lemma cvg_eq x y : x --> y -> x = y.
-Proof. by rewrite -closeE //; apply: cvg_close. Qed.
-
-Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
-  {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
-Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
-
-
-Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}.
-Proof.
-move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //.
-- apply: filter_from_proper => //; first last.
-    by move=> ? /nbhs_singleton/subset_closure ?; exists x.
-  apply: filter_from_filter; first by exists setT; exact: filterT.
-  move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI].
-- by exists V => //; have /closure_id <- : closed V by exact: compact_closed.
-rewrite eqEsubset; split; first last.
-  move=> _ -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //.
-  by apply/CA/subset_closure; exact: nbhs_singleton.
-move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply].
-move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0].
-apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP.
-split; first by exists A => //; exact: open_nbhs_nbhs.
-apply/not_implyP; split; first exact: open_nbhs_nbhs.
-apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset.
-have /closure_id -> : closed (~` B); first by exact: open_closedC.
-by apply/closure_subset/disjoints_subset; rewrite setIC.
-Qed.
-
-End separated_topologicalType.
-
-Section separated_ptopologicalType.
-Variable T : ptopologicalType.
-Implicit Types x y : T.
-
-Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} :
-  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
-Proof.
-move=> F12 F21.
-have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
-  by apply: (@cvg_close _ F2) => //; apply: cvgP F2l.
-have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
-rewrite dvgP // dvgP //; exact/close_refl.
-Qed.
-
-Hypothesis sep : hausdorff_space T.
-
-Lemma lim_id x : lim (nbhs x) = x.
-Proof. by apply/esym/cvg_eq/cvg_ex => //; exists x. Qed.
-
-Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
-  f @ F --> l -> lim (f @ F) = l.
-Proof. by move=> /[dup] /cvgP /cvg_unique; apply. Qed.
-
-Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
-   (\forall x \near F, f x = l) -> lim (f @ F) = l.
-Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
-
-Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
-   lim ((fun _ : U => k) @ F) = k.
-Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
-
-Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
-  F (fun x : U => is_subset1 (f x)) ->
-  f `@ F --> l -> lim (f `@ F) = l.
-Proof.
-move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
-Qed.
-
-End separated_ptopologicalType.
-
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
-Notation cvg_map_lim := cvg_lim (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgi_lim`")]
-Notation cvgi_map_lim := cvgi_lim (only parsing).
-
 Section connected_sets.
 Variable T : topologicalType.
 Implicit Types A B C D : set T.
@@ -2265,11 +1969,6 @@ rewrite dsc nbhs_simpl; split; first by exact.
 by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->.
 Qed.
 
-Lemma discrete_hausdorff : hausdorff_space X.
-Proof.
-by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q))[x [] -> ->].
-Qed.
-
 HB.instance Definition _ := Nbhs_isNbhsTopological.Build bool
   principal_filter_proper discrete_sing discrete_nbhs.
 
@@ -2291,94 +1990,6 @@ Qed.
 
 #[global] Hint Resolve discrete_bool : core.
 
-Section perfect_sets.
-
-Implicit Types (T : topologicalType).
-
-Definition perfect_set {T} (A : set T) := closed A /\ limit_point A = A.
-
-Lemma perfectTP {T} : perfect_set [set: T] <-> forall x : T, ~ open [set x].
-Proof.
-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.
-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.
-  by split => // ? ->.
-by exists y; split => //; [exact/eqP | exact: VU].
-Qed.
-
-Lemma perfect_set2 {T} : perfect_set [set: T] <->
-  forall (U : set T), open U -> U !=set0 ->
-  exists x y, [/\ U x, U y & x != y] .
-Proof.
-apply: iff_trans; first exact: perfectTP; split.
-  move=> nx1 U oU [] x Ux; exists x.
-  have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1.
-  apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset.
-  (split => //; last by move=> ? ->); move=> y Uy; have  /not_and3P := Uyx y.
-  by case => // /negP; rewrite negbK => /eqP ->.
-move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
-by move=> y [] ? [->] -> /eqP.
-Qed.
-
-End perfect_sets.
-
-Section totally_disconnected.
-Implicit Types T : topologicalType.
-
-Definition totally_disconnected {T} (A : set T) :=
-  forall x, A x -> connected_component A x = [set x].
-
-Definition zero_dimensional T :=
-  (forall x y, x != y -> exists U : set T, [/\ clopen U, U x & ~ U y]).
-
-Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T.
-Proof.
-move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP.
-by split; [exact: discrete_open | exact: discrete_closed].
-Qed.
-
-Lemma zero_dimension_totally_disconnected {T} :
-  zero_dimensional T -> totally_disconnected [set: T].
-Proof.
-move=> zdA x _; rewrite eqEsubset.
-split=> [z [R [Rx _ ctdR Rz]]|_ ->]; last exact: connected_component_refl.
-apply: contrapT => /eqP znx; have [U [[oU cU] Uz Ux]] := zdA _ _  znx.
-suff : R `&` U = R by move: Rx => /[swap] <- [].
-by apply: ctdR; [exists z|exists U|exists U].
-Qed.
-
-Lemma totally_disconnected_cvg {T : topologicalType} (x : T) :
-  hausdorff_space T -> zero_dimensional T -> compact [set: T] ->
-  filter_from [set D : set T | D x /\ clopen D] id --> x.
-Proof.
-pose F := filter_from [set D : set T | D x /\ clopen D] id.
-have FF : Filter F.
-  apply: filter_from_filter; first by exists setT; split => //; exact: clopenT.
-  by move=> A B [? ?] [? ?]; exists (A `&` B) => //; split=> //; exact: clopenI.
-have PF : ProperFilter F by apply: filter_from_proper; move=> ? [? _]; exists x.
-move=> hsdfT zdT cmpT U Ux; rewrite nbhs_simpl -/F.
-wlog oU : U Ux / open U.
-  move: Ux; rewrite /= nbhsE => -[] V [? ?] /filterS + /(_ V) P.
-  by apply; apply: P => //; exists V.
-have /(iffLR (compact_near_coveringP _)) : compact (~` U).
-  by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC.
-move=> /(_ _ _ setC (powerset_filter_from_filter PF))[].
-  move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y.
-    by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton.
-  exists (~` C, [set U | U `<=` C]); first split.
-  - by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
-  - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans.
-    by exists C => //; exists C.
-  - by case=> i j [? /subsetC]; apply.
-by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF.
-Qed.
-
-End totally_disconnected.
 
 (** TODO: generalize this to a preOrder once that's available *)
 HB.mixin Record Order_isNbhs d (T : Type) of Nbhs T & Order.Total d T := {
@@ -2487,27 +2098,6 @@ case: p E.
   by split => //; exact/(le_trans _ pl)/upL.
 Qed.
 
-Lemma order_hausdorff : hausdorff_space T.
-Proof.
-rewrite open_hausdorff=> p q; wlog : p q / p < q.
-  have /orP[] := le_total p q; rewrite le_eqVlt => /predU1P[->|].
-  - by rewrite eqxx.
-  - by move=> ?; exact.
-  - by rewrite eqxx.
-  - move=> qp WH; rewrite eq_sym => /(WH _ _ qp)[[P Q] [? ?] [? ? ?]].
-    by exists (Q, P); split; rewrite // setIC.
-move=> plq ?; have [[z /andP[pz zq]]|] := pselect (exists z, p < z < q).
-  exists (`]-oo,z[, `]z,+oo[).
-    by split => //=; apply/mem_set; rewrite set_itvE.
-  split => //= ; apply/eqP; rewrite -subset0 => r; rewrite set_itvE => -[/= rz].
-  by apply/negP; rewrite in_itv/= andbT -leNgt (ltW rz).
-move=> npzq; exists (`]-oo, q[, `]p, +oo[); split => //=.
-- by apply /mem_set; rewrite set_itvE.
-- by apply /mem_set; rewrite set_itvE.
-- apply/eqP; rewrite -subset0 => r; rewrite !set_itvE => -[/= rz zr].
-  by apply: npzq; exists r; rewrite rz zr.
-Qed.
-
 Let sub_open_mem x (U : set T) (i : interval T) :=
   [/\ [set` i] `<=` U, open [set` i] & x \in i].
 
@@ -2531,38 +2121,6 @@ by rewrite itv_setU ?{1}subUset //; [exact: openU | exists w].
 exact/(le_trans jy)/leUr.
 Qed.
 
-Lemma zero_dimensional_ray x y : x < y -> zero_dimensional T ->
-  exists U, [/\ clopen U, U y , ~ U x & forall l r, U r -> ~ U l -> l < r].
-Proof.
-move=> xy zt; have xNy : y != x by move: xy; rewrite lt_def => /andP[].
-have [U [clU Uy nUx]] := zt y x xNy.
-pose I := \bigcup_(i in sub_open_mem y U) [set` i].
-have Iy : I y.
-  case: clU => + _; rewrite openE => /(_ _ Uy).
-  rewrite /interior /= itv_nbhsE /= => -[i [] iy yi iU].
-  by exists i => //; split => //; exact: itv_open_ends_open.
-have IU : I `<=` U by move=> ? [? [+ _ _]] => /subset_trans; exact.
-pose V := I `|` `[y, +oo[; exists V.
-have [? ?] := clopen_bigcup_clopen clU Uy.
-split; first split.
-- suff -> : V = I `|` `]y,+oo[ by exact: openU.
-  rewrite eqEsubset; split => z; case; first by left.
-  + by rewrite -setU1itv // => -[->|]; [left| right].
-  + by left.
-  + by rewrite /V -setU1itv //; right; right.
-- by apply: closedU => //; exact: rray_closed.
-- by left.
-- by move=> [/IU //|]; rewrite set_itvE/= leNgt xy.
-- move=> l r Vr Vl; rewrite ltNge; apply/negP; move: Vl; apply: contra_not.
-  move=> rl; case: Vr; first last.
-    by rewrite set_itvE => yr; right; rewrite set_itvE; exact: (le_trans yr).
-  have /orP[|ly] := le_total y l; first by move=> + _; right; rewrite set_itvE.
-  case=> i [iu oi /= yi ri]; left; exists i; first by split.
-  move: iu oi => _ _; case: i yi ri => p q /= /andP [py yq] /andP[pr rq].
-  apply/andP; split.
-  + by rewrite (le_trans pr)// bnd_simp.
-  + by rewrite (le_trans _ yq)// bnd_simp.
-Qed.
 
 End order_topologies.
 Hint Resolve lray_open : core.
@@ -2958,54 +2516,13 @@ exists (range f); split; first exact: card_image_le.
 by move=> E /fsubE [n fnA]; exists (f n) => //; exists n.
 Qed.
 
-Section uniform_closeness.
-Variable (U : uniformType).
-
-Lemma open_nbhs_entourage (x : U) (A : set (U * U)) :
+Lemma open_nbhs_entourage (U : uniformType) (x : U) (A : set (U * U)) :
   entourage A -> open_nbhs x (xsection A x)^°.
 Proof.
 move=> entA; split; first exact: open_interior.
 by apply: nbhs_singleton; apply: nbhs_interior; apply: nbhs_entourage.
 Qed.
 
-Lemma entourage_close (x y : U) : close x y = forall A, entourage A -> A (x, y).
-Proof.
-rewrite propeqE; split=> [cxy A entA|cxy].
-  have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy.
-  have yl := nbhs_entourage _ (entourage_inv entsA).
-  have yr := nbhs_entourage _ entsA.
-  have [z [/xsectionP zx /xsectionP zy]] := cxy _ _ (yr x) (yl y).
-  exact: (entourage_split z).
-rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B].
-exists y; split.
-- by apply/sE1A/xsectionP; exact: cxy.
-- by apply/sE2B/xsectionP; exact: entourage_refl.
-Qed.
-
-Lemma close_trans (y x z : U) : close x y -> close y z -> close x z.
-Proof.
-rewrite !entourage_close => cxy cyz A entA.
-exact: entourage_split (cxy _ _) (cyz _ _).
-Qed.
-
-Lemma close_cvgxx (x y : U) : close x y -> x --> y.
-Proof.
-rewrite entourage_close => cxy P /= /nbhsP[A entA sAP].
-apply/nbhsP; exists (split_ent A) => // z /xsectionP xz; apply: sAP.
-apply/xsectionP; apply: (entourage_split x) => //.
-by have := cxy _ (entourage_inv (entourage_split_ent entA)).
-Qed.
-
-End uniform_closeness.
-
-Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
-  F --> l <-> ([cvg F in U] /\ close (lim F) l).
-Proof.
-move=> FF; split=> [Fl|[cvF]Cl].
-  by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F).
-by apply: cvg_trans (close_cvgxx Cl).
-Qed.
-
 
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
   (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.
@@ -3669,6 +3186,8 @@ Proof. by move/cvgi_ballP. Qed.
 
 End pseudoMetricType_numDomainType.
 
+#[global] Hint Resolve nbhsx_ballx : core.
+
 Global Instance entourage_proper_filter {R : numDomainType}
   {M : pseudoPMetricType R} : ProperFilter (@entourage M).
 Proof.
@@ -3676,10 +3195,6 @@ apply: Build_ProperFilter_ex; rewrite -entourage_ballE => A [_/posnumP[e] sbeA].
 by exists (point, point); apply: sbeA; apply: ballxx.
 Qed.
 
-#[global] Hint Resolve nbhsx_ballx : core.
-#[global] Hint Resolve close_refl : core.
-Arguments close_cvg {T} F1 F2 {FF2} _.
-
 Arguments nbhsx_ballx {R M} x eps.
 Arguments near_ball {R M} y eps.
 
@@ -3701,42 +3216,9 @@ Lemma ball_splitl (z x y : M) (e : R) :
   ball x (e / 2) z -> ball y (e / 2) z -> ball x e y.
 Proof. by move=> bxz /ball_sym /(ball_split bxz). Qed.
 
-Lemma ball_close (x y : M) :
-  close x y = forall eps : {posnum R}, ball x eps%:num y.
-Proof.
-rewrite propeqE; split => [cxy eps|cxy].
-  have := !! cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos).
-  rewrite closureEonbhs/= meetsC meets_globallyr.
-  move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]].
-  by apply: (@ball_splitl z); apply: interior_subset.
-rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]]
-  /nbhs_ballP[_/posnumP[e1 e1A]].
-by exists y; split; [apply/e2B|apply/e1A; exact: ballxx].
-Qed.
 
 End pseudoMetricType_numFieldType.
 
-Section ball_hausdorff.
-Variables (R : numDomainType) (T : pseudoMetricType R).
-
-Lemma ball_hausdorff : hausdorff_space T =
-  forall (a b : T), a != b ->
-  exists r : {posnum R} * {posnum R},
-    ball a r.1%:num `&` ball b r.2%:num == set0.
-Proof.
-rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
-  move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]].
-  have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by apply: open_nbhs_nbhs.
-  have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by apply: open_nbhs_nbhs.
-  by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0).
-move=> r s /eqP brs_eq0; exists ((ball a r%:num)^°, (ball b s%:num)^°) => /=.
-  split; by rewrite inE; apply: nbhs_singleton; apply: nbhs_interior;
-            apply/nbhs_ballP; apply: in_filter_from => /=.
-split; do ?by apply: open_interior.
-by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset.
-Qed.
-End ball_hausdorff.
-
 Section entourages.
 Variable R : numDomainType.
 Lemma unif_continuousP (U V : pseudoMetricType R) (f : U -> V) :
@@ -4285,9 +3767,6 @@ rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //.
 by rewrite {2}(splitr e%:num) ltr_pwDl.
 Qed.
 
-Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
-Proof. exact: order_hausdorff. Qed.
-
 Definition dense (T : topologicalType) (S : set T) :=
   forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.
 
@@ -4411,361 +3890,6 @@ suff : @clopen T = set0 \/ $|{surjfun [set: nat] >-> @clopen T}|.
 exact/pfcard_geP/clopen_countable/compact_second_countable.
 Qed.
 
-(* This section proves that uniform spaces, with a countable base for their
-   entourage, are metrizable. The definition of this metric is rather arcane,
-   and the proof is tough. That's ok because the resulting metric is not
-   intended to be used explicitly. Instead, this is typically used in
-   applications that do not depend on the metric:
-   - `metric spaces are T4`
-   - `in metric spaces, compactness and sequential compactness agree`
-   - infinite products of metric spaces are metrizable
-*)
-Module countable_uniform.
-Section countable_uniform.
-Local Open Scope relation_scope.
-Context {R : realType} {T : uniformType}.
-
-Hypothesis cnt_unif : @countable_uniformity T.
-
-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 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.
-
-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`
-   - each (g_ n) is symmetric
-   - the sets (g_ n) are nested downward
-   - g_ n.+1 \o g_ n.+1 \o g_ n.+1 `<=` g_ n says the sets descend `quickly`
- *)
-
-Local Fixpoint g_ n : set (T * T) :=
-  if n is n.+1 then let W := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1
-  else [set: T*T].
-
-Let entG n : entourage (g_ n).
-Proof.
-elim: n => /=; first exact: entourageT.
-by move=> n entg; apply/entourage_invI; exact: filterI.
-Qed.
-
-Local Lemma symG n : (g_ n)^-1 = g_ n.
-Proof.
-by case: n => // n; rewrite eqEsubset; split; case=> ? ?; rewrite /= andC.
-Qed.
-
-Local Lemma descendG1 n : g_ n.+1 `<=` g_ n.
-Proof.
-apply: subIset; left; apply: subIset; left; apply: subset_trans.
-  by apply: split_ent_subset; exact: entourage_split_ent.
-by apply: subset_trans; last exact: split_ent_subset.
-Qed.
-
-Local Lemma descendG n m : (m <= n)%N -> g_ n `<=` g_ m.
-Proof.
-elim: n; rewrite ?leqn0; first by move=>/eqP ->.
-move=> n IH; rewrite leq_eqVlt ltnS => /orP [/eqP <- //|] /IH.
-by apply: subset_trans; exact: descendG1.
-Qed.
-
-Local Lemma splitG3 n : g_ n.+1 \; g_ n.+1 \; g_ n.+1 `<=` g_ n.
-Proof.
-suff g2split : g_ n.+1 \; g_ n.+1 `<=` split_ent (g_ n).
-  apply: subset_trans; last exact: subset_split_ent (entG n).
-  apply: set_compose_subset (g2split); rewrite -[_ n.+1]set_compose_diag.
-  apply: subset_trans g2split; apply: set_compose_subset => //.
-  by move=> [_ _] [z _] [<- <-]; exact: entourage_refl.
-apply: subset_trans; last exact: subset_split_ent.
-by apply: set_compose_subset; apply: subIset; left; apply: subIset; left.
-Qed.
-
-Local Lemma gsubf n : g_ n.+1 `<=` f_ n.
-Proof. by apply: subIset; left; apply: subIset; right. Qed.
-
-Local Lemma countableBaseG A : entourage A -> exists N, g_ N `<=` A.
-Proof.
-move=> /countableBase [N] fnA; exists N.+1.
-by apply: subset_trans fnA; exact: gsubf.
-Qed.
-
-(* Step 2.
-   We build a sensible notion of balls for our metric.
-   The naive attempt,
-                     `ball x e y := g_ (distN e) (x,y))
-   doesn't respect triangle inequality. We need to cook triangle inequality
-   into the balls themselves. So we define balls in terms of steps:
-      `ball x e y := there are n steps x_0 = x,...,x_i,..., x_n.+1 = y and
-                     e_1,...,e_n such that
-                           g_ (distN e_i) (x_i,x_i+1)
-                                    and
-                               sum (e_i) = e
-*)
-
-Local Open Scope classical_set_scope.
-Local Open Scope ring_scope.
-
-Local Definition distN (e : R) : nat := `|Num.floor e^-1|%N.
-
-Local Lemma distN0 : distN 0 = 0%N.
-Proof. by rewrite /distN invr0 floor0. Qed.
-
-Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n.
-Proof.
-rewrite /distN invrK.
-apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm ?floor_ge0//.
-by rewrite -intrEfloor intrEge0.
-Qed.
-
-Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.
-Proof.
-move=> e1pos e1e2; rewrite /distN; apply: lez_abs2.
-  by rewrite floor_ge0 ltW// invr_gt0 (lt_le_trans _ e1e2).
-by rewrite floor_le// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2).
-Qed.
-
-Local Fixpoint n_step_ball n x e z :=
-  if n is n.+1 then exists y d1 d2,
-    [/\ n_step_ball n x d1 y,
-        0 < d1,
-        0 < d2,
-        g_ (distN d2) (y, z) &
-        d1 + d2 = e]
-  else e > 0 /\ g_ (distN e) (x, z).
-
-Local Definition step_ball x e z := exists i, (n_step_ball i x e z).
-
-Local Lemma n_step_ball_pos n x e z : n_step_ball n x e z -> 0 < e.
-Proof.
-by case: n => [[]|] // n; case=> [?] [?] [?] [] ? ? ? ? <-; apply: addr_gt0.
-Qed.
-
-Local Lemma step_ball_pos x e z : step_ball x e z -> 0 < e.
-Proof. by case => ?; exact: n_step_ball_pos. Qed.
-
-Local Lemma entourage_nball e :
-  0 < e -> entourage [set xy | step_ball xy.1 e xy.2].
-Proof.
-move=> epos; apply: (@filterS _ _ _ (g_ (distN e))) => // [[x y]] ?.
-by exists 0%N.
-Qed.
-
-Local Lemma n_step_ball_center x e : 0 < e -> n_step_ball 0 x e x.
-Proof. by move=> epos; split => //; exact: entourage_refl. Qed.
-
-Local Lemma step_ball_center x e : 0 < e -> step_ball x e x.
-Proof. by move=> epos; exists 0%N; apply: n_step_ball_center. Qed.
-
-Local Lemma n_step_ball_triangle n m x y z d1 d2 :
-  n_step_ball n x d1 y ->
-  n_step_ball m y d2 z ->
-  n_step_ball (n + m).+1 x (d1 + d2) z.
-Proof.
-move: n z d2; elim: m => [n z d2 Nxy [? ?]|n IH m z d2 Oxy].
-  by exists y, d1, d2; split; rewrite ?addn0 // (n_step_ball_pos Nxy).
-move=> [w] [e1] [e2] [Oyw ? ? ? <-].
-exists w, (d1 + e1), e2; rewrite addnS addrA.
-split => //; last by rewrite addr_gt0//; exact: n_step_ball_pos Oxy.
-by case: (IH m w e1 Oxy Oyw) => t [e3] [e4] [] Oxt ? ? ? <-; exists t, e3, e4.
-Qed.
-
-Local Lemma step_ball_triangle x y z d1 d2 :
-  step_ball x d1 y -> step_ball y d2 z -> step_ball x (d1 + d2) z.
-Proof.
-move=> [n Oxy] [m Oyz]; exists (n + m).+1.
-exact: n_step_ball_triangle Oxy Oyz.
-Qed.
-
-Local Lemma n_step_ball_sym n x y e :
-  n_step_ball n x e y -> n_step_ball n y e x.
-Proof.
-move: x y e; elim: n; first by move=> ? ? ?; rewrite /= -{1}symG.
-move=> n IH x y e [t] [d1] [d2] [] /IH Oty ? ?.
-rewrite addrC -symG -[n]add0n => gty <-; apply: (n_step_ball_triangle _ Oty).
-by split => //; exact: gty.
-Qed.
-
-Local Lemma step_ball_sym x y e : step_ball x e y -> step_ball y e x.
-Proof. by case=> n /n_step_ball_sym ?; exists n. Qed.
-
-(* Step 3:
-   We prove that step_ball respects the original entourage. This requires an
-   induction on the length of the steps, which is pretty tricky. The central
-   lemma is `split_n_step_ball`, which lets us break a list into parts three
-   parts as: half + one_step + half. Then our we can break apart our n +1 path
-
-                         nlong + one_step
-   into
-                  (half + one_step + half) + one_step
-                                =
-                  half + one_step + (half + one_step)
-
-   and we can we can use our (strong) induction hypothesis.
-   And lastly we finish with splitG3.
-*)
-
-Local Lemma n_step_ball_le n x e1 e2 :
-  e1 <= e2 -> n_step_ball n x e1 `<=` n_step_ball n x e2.
-Proof.
-move: x e1 e2; elim: n.
-  move=> x e1 e2 e1e2 y [?] gxy; split; first exact: (lt_le_trans _ e1e2).
-  by apply: descendG; last (exact: gxy); exact: distN_le.
-move=> n IH x e1 e2 e1e2 z [y] [d1] [d2] [] /IH P d1pos d2pos gyz d1d2e1.
-have d1e1d2 : d1 = e1 - d2 by rewrite -d1d2e1 -addrA subrr addr0.
-have e2d2le : e1 - d2 <= e2 - d2 by exact: lerB.
-exists y, (e2 - d2), d2; split => //.
-- by apply: P; apply: le_trans e2d2le; rewrite d1e1d2.
-- by apply: lt_le_trans e2d2le; rewrite -d1e1d2.
-- by rewrite -addrA [-_ + _]addrC subrr addr0.
-Qed.
-
-Local Lemma step_ball_le x e1 e2 :
-  e1 <= e2 -> step_ball x e1 `<=` step_ball x e2.
-Proof. by move=> e1e2 ? [n P]; exists n; exact: (n_step_ball_le e1e2). Qed.
-
-Local Lemma distN_half (n : nat) : n.+1%:R^-1 / (2:R) <= n.+2%:R^-1.
-Proof.
-rewrite -invrM //; [|exact: unitf_gt0 |exact: unitf_gt0].
-rewrite lef_pV2 ?posrE // -?natrM ?ler_nat -addn1 -addn1 -addnA mulnDr.
-by rewrite muln1 leq_add2r leq_pmull.
-Qed.
-
-Local Lemma split_n_step_ball n x e1 e2 z :
-  0 < e1 -> 0 < e2 -> n_step_ball n.+1 x (e1 + e2) z ->
-    exists t1 t2 a b,
-    [/\
-      n_step_ball a x e1 t1,
-      n_step_ball 0 t1 (e1 + e2) t2,
-      n_step_ball b t2 e2 z &
-      (a + b = n)%N
-    ].
-Proof.
-move: e1 e2 x z; elim: n.
-  move=> e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Oxy ? ? gd2yz deE.
-  case: (pselect (e1 <= d1)).
-    move=> e1d1; exists x, y, 0%N, 0%N; split.
-    - exact: n_step_ball_center.
-    - apply: n_step_ball_le; last exact: Oxy.
-      by rewrite -deE lerDl; apply: ltW.
-    - apply: (@n_step_ball_le _ _ d2); last by split.
-      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK [leLHS]addrC.
-      by rewrite [e2 + _]addrC -deE; exact: lerD.
-    - by rewrite addn0.
-  move=> /negP; rewrite -ltNge//.
-  move=> e1d1; exists y, z, 0%N, 0%N; split.
-  - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW.
-  - rewrite -deE; apply: (@n_step_ball_le _ _ d2) => //.
-    by rewrite lerDr; apply: ltW.
-  - exact: n_step_ball_center.
-  - by rewrite addn0.
-move=> n IH e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Od1xy d1pos d2pos gd2yz deE.
-case: (pselect (e2 <= d2)).
-  move=> e2d2; exists y, z, n.+1, 0%N; split.
-  - apply: (@n_step_ball_le _ _ d1); rewrite // -[e1]addr0 -(subrr e2) addrA.
-    by rewrite -deE -lerBlDr opprK lerD.
-  - apply: (@n_step_ball_le _ _ d2); last by split.
-    by rewrite -deE lerDr; exact: ltW.
-  - exact: n_step_ball_center.
-  - by rewrite addn0.
-have d1E' : d1 = e1 + (e2 - d2).
-  by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0.
-move=> /negP; rewrite -ltNge// => d2lee2.
-  case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
-  move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
-  exists t1, t2, c1, c2.+1; split => //.
-  - by apply: (@n_step_ball_le _ _ d1); rewrite -?deE // ?lerDl; exact: ltW.
-  - exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0//.
-    by rewrite -addrA [-_ + _]addrC subrr addr0.
-  - by rewrite addnS.
-Qed.
-
-Local Lemma n_step_ball_le_g x n :
-  n_step_ball 0 x n%:R^-1 `<=` [set y | g_ n (x,y)].
-Proof. by move=> y [] ?; rewrite distN_nat. Qed.
-
-Local Lemma subset_n_step_ball n x N :
-  n_step_ball n x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
-Proof.
-move: N x; elim: n {-2}n (leqnn n) => n.
-  rewrite leqn0 => /eqP -> N x; apply: subset_trans.
-    exact: n_step_ball_le_g.
-  by move=> y ?; exact: descendG.
-move=> IH1 + + N x1 x4; case.
-  by move=> ? [?] P; apply: descendG _ P; rewrite distN_nat.
-move=> l ln1 Ox1x4.
-case: (@split_n_step_ball l x1 (N.+1%:R^-1/2) (N.+1%:R^-1/2) x4) => //.
-  by rewrite -splitr.
-move=> x2 [x3] [l1] [l2] [] P1 [? +] P3 l1l2; rewrite -splitr distN_nat => ?.
-have l1n : (l1 <= n)%N by rewrite (leq_trans (leq_addr l2 l1))// l1l2 -ltnS.
-have l2n : (l2 <= n)%N by rewrite (leq_trans (leq_addl l1 l2))// l1l2 -ltnS.
-apply: splitG3; exists x3; [exists x2 => //|].
-  by move/(n_step_ball_le (distN_half N))/(IH1 _ l1n) : P1.
-by move/(n_step_ball_le (distN_half N))/(IH1 _ l2n) : P3.
-Qed.
-
-Local Lemma subset_step_ball x N :
-  step_ball x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
-Proof. by move=> y [] n; exact: subset_n_step_ball. Qed.
-
-Local Lemma step_ball_entourage : entourage = entourage_ step_ball.
-Proof.
-rewrite predeqE => E; split; first last.
-  by case=> e /= epos esubE; apply: (filterS esubE); exact: entourage_nball.
-move=> entE; case: (countableBase entE) => N fN.
-exists N.+2%:R^-1; first by rewrite /= invr_gt0.
-apply: (subset_trans _ fN); apply: subset_trans; last apply: gsubf.
-by case=> x y /= N1ball; apply: (@subset_step_ball x N.+1).
-Qed.
-
-Definition type : Type := let _ := countableBase in let _ := entF in T.
-
-#[export] HB.instance Definition _ := Uniform.on type.
-#[export] HB.instance Definition _ := Uniform_isPseudoMetric.Build R type
-  step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.
-#[export] HB.instance Definition _ {q : Pointed T} := Pointed.copy type (Pointed.Pack q).
-
-Lemma countable_uniform_bounded (x y : T) :
-  let U := [the pseudoMetricType R of type]
-  in @ball _ U x 2 y.
-Proof.
-rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
-rewrite [X in `|X|%N](_ : _ = 0) ?absz0//.
-apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt.
-by apply/andP; split => //; rewrite invf_lt1 //= ltrDl.
-Qed.
-
-End countable_uniform.
-
-
-Module Exports. HB.reexport. End Exports.
-End countable_uniform.
-Export countable_uniform.Exports.
-
-Notation countable_uniform := countable_uniform.type.
-
-Definition sup_pseudometric (R : realType) (T : Type) (Ii : Type)
-  (Tc : Ii -> PseudoMetric R T) (Icnt : countable [set: Ii]) : Type := T.
-
-Section sup_pseudometric.
-Variable (R : realType) (T : choiceType) (Ii : Type).
-Variable (Tc : Ii -> PseudoMetric R T).
-
-Hypothesis Icnt : countable [set: Ii].
-
-Local Notation S := (sup_pseudometric Tc Icnt).
-
-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)).
-
-HB.instance Definition _ : PseudoMetric R S :=
-  PseudoMetric.on (countable_uniform countable_uniformityT).
-
-End sup_pseudometric.
-
 Definition subspace {T : Type} (A : set T) := T.
 Arguments subspace {T} _ : simpl never.
 
@@ -4995,13 +4119,6 @@ apply: subset_trans (@subIsetl _ V A); rewrite VAclUA subsetI; split => //.
 exact: (@subset_closure _ (U : set (subspace A))).
 Qed.
 
-Lemma subspace_hausdorff :
-  hausdorff_space T -> hausdorff_space [the topologicalType of subspace A].
-Proof.
-rewrite ?open_hausdorff => + x y xNy => /(_ x y xNy).
-move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ].
-by move=> ?; exists (P, Q).
-Qed.
 End SubspaceOpen.
 
 Lemma compact_subspaceIP (U : set T) :
@@ -5384,114 +4501,3 @@ move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U.
 move/nbhs_singleton: nbhsU; move: x; apply/in_setP.
 by rewrite -continuous_open_subspace.
 Unshelve. end_near. Qed.
-
-Module gauge.
-Section gauge.
-Local Open Scope relation_scope.
-
-Let split_sym {T : uniformType} (W : set (T * T)) :=
-  (split_ent W) `&` (split_ent W)^-1.
-
-Section entourage_gauge.
-Context {T : uniformType} (E : set (T * T)) (entE : entourage E).
-
-Definition gauge :=
-  filter_from [set: nat] (fun n => iter n split_sym (E `&` E^-1)).
-
-Lemma iter_split_ent j : entourage (iter j split_sym (E `&` E^-1)).
-Proof. by elim: j => [|i IH]; exact: filterI. Qed.
-
-Lemma gauge_ent A : gauge A -> entourage A.
-Proof.
-case=> n; elim: n A; first by move=> ? _ /filterS; apply; apply: filterI.
-by move=> n ? A _ /filterS; apply; apply: filterI; have ? := iter_split_ent n.
-Qed.
-
-Lemma gauge_filter : Filter gauge.
-Proof.
-apply: filter_from_filter; first by exists 0%N.
-move=> i j _ _; wlog ilej : i j / (i <= j)%N.
-  by move=> WH; have [|/ltnW] := leqP i j;
-    [|rewrite (setIC (iter _ _ _))]; exact: WH.
-exists j => //; rewrite subsetI; split => //; elim: j i ilej => [i|j IH i].
-  by rewrite leqn0 => /eqP ->.
-rewrite leq_eqVlt => /predU1P[<-//|/ltnSE/IH]; apply: subset_trans.
-by move=> x/= [jx _]; apply: split_ent_subset => //; exact: iter_split_ent.
-Qed.
-
-Lemma gauge_refl A : gauge A -> diagonal `<=` A.
-Proof.
-case=> n _; apply: subset_trans => -[_ a]/diagonalP ->.
-by apply: entourage_refl; exact: iter_split_ent.
-Qed.
-
-Lemma gauge_inv A : gauge A -> gauge A^-1.
-Proof.
-case=> n _ EA; apply: (@filterS _ _ _ (iter n split_sym (E `&` E^-1))).
-- exact: gauge_filter.
-- by case: n EA; last move=> n; move=> EA [? ?] [/=] ? ?; exact: EA.
-- by exists n .
-Qed.
-
-Lemma gauge_split A : gauge A -> exists2 B, gauge B & B \; B `<=` A.
-Proof.
-case => n _ EA; exists (iter n.+1 split_sym (E `&` E^-1)); first by exists n.+1.
-apply: subset_trans EA; apply: subset_trans; first last.
-  by apply: subset_split_ent; exact: iter_split_ent.
-by case=> a c [b] [] ? ? [] ? ?; exists b.
-Qed.
-
-Let gauged : Type := T.
-
-HB.instance Definition _ := Choice.on gauged.
-HB.instance Definition _ :=
-  @isUniform.Build gauged gauge gauge_filter gauge_refl gauge_inv gauge_split.
-
-Lemma gauge_countable_uniformity : countable_uniformity gauged.
-Proof.
-exists [set iter n split_sym (E `&` E^-1) | n in [set: nat]].
-split; [exact: card_image_le | by move=> W [n] _ <-; exists n|].
-by move=> D [n _ ?]; exists (iter n split_sym (E `&` E^-1)).
-Qed.
-
-Definition type := countable_uniform.type gauge_countable_uniformity.
-End entourage_gauge.
-
-End gauge.
-Module Exports. HB.reexport. End Exports.
-End gauge.
-Export gauge.Exports.
-
-Lemma uniform_pseudometric_sup {R : realType} {T : puniformType} :
-    @entourage T = @sup_ent T {E : set (T * T) | @entourage T E}
-  (fun E => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).
-Proof.
-rewrite eqEsubset; split => [E entE|E].
-  exists E => //=.
-  pose pe : {classic {E0 : set (T * T) | _}} * _ := (exist _ E entE, E).
-  have entPE : `[< @entourage (gauge.type entE) E >].
-    by apply/asboolP; exists 0%N => // ? [].
-  exists (fset1 (exist _ pe entPE)) => //=; first by move=> ?; rewrite in_setE.
-  by rewrite set_fset1 bigcap_set1.
-case=> W /= [/= J] _ <- /filterS; apply; apply: filter_bigI => -[] [] [] /= D.
-move=> entD G /[dup] /asboolP [n _ + _ _] => /filterS; apply.
-exact: gauge.iter_split_ent.
-Qed.
-
-Local Open Scope relation_scope.
-Lemma uniform_regular {T : uniformType} : @regular_space T.
-Proof.
-move=> x R /=; rewrite -{1}nbhs_entourageE => -[E entE ER].
-pose E' := split_ent E; have eE' : entourage E' by exact: entourage_split_ent.
-exists (xsection (E' `&` E'^-1) x).
-  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
-  exact: filterI.
-move=> z /= clEz; apply/ER/xsectionP; apply: subset_split_ent => //.
-have [] := clEz (xsection (E' `&` E'^-1) z).
-  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
-  exact: filterI.
-by move=> y /= [/xsectionP[? ?] /xsectionP[? ?]]; exists y.
-Qed.
-Local Close Scope relation_scope.
-
-#[global] Hint Resolve uniform_regular : core.

From 68b3afbae07d18f684e7b33a53f141e32176b181 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 3 Oct 2024 23:01:22 -0400
Subject: [PATCH 2/7] adding changelog

---
 CHANGELOG_UNRELEASED.md      | 22 ++++++++++++++++++++++
 theories/separation_axioms.v | 13 ++-----------
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8924b1821..542e55de0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -168,7 +168,29 @@
 - moved from `topology.v` to `boolp.v`:
   + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
 
+- moved from `topology.v` to `separation_axioms.v`: `set_nbhs`, `set_nbhsP`,
+    `accessible_space`, `kolmogorov_space`, `hausdorff_space`,
+    `compact_closed`, `discrete_hausdorff`, `compact_cluster_set1`,
+    `compact_precompact`, `open_hausdorff`, `hausdorff_accessible`,
+    `accessible_closed_set1`, `accessible_kolmogorov`,
+    `accessible_finite_set_closed`, `subspace_hausdorff`, `order_hausdorff`,
+    `ball_hausdorff`, `Rhausdorff`, `close`, `closeEnbhs`, `closeEonbhs`,
+    `close_sym`, `cvg_close`, `close_refl`, `cvgx_close`, `cvgi_close`,
+    `cvg_toi_locally_close`, `closeE`, `close_eq`, `cvg_unique`, `cvg_eq`,
+    `cvgi_unique`, `close_cvg`, `lim_id`, `lim_near_cst`, `lim_cst`,
+    `entourage_close`, `close_trans`, `close_cvgxx`, `cvg_closeP`,
+    `ball_close`, `normal_space`, `regular_space`, `compact_regular`,
+    `uniform_regular`, `totally_disconnected`, `zero_dimensional`,
+    `discrete_zero_dimension`, `zero_dimension_totally_disconnected`,
+    `zero_dimensional_ray`, `type`, `countable_uniform_bounded`,
+    `countable_uniform`, `sup_pseudometric`, `countable_uniformityT`, `gauge`,
+    `iter_split_ent`, `gauge_ent`, `gauge_filter`, `gauge_refl`, `gauge_inv`,
+    `gauge_split`, `gauge_countable_uniformity`, `uniform_pseudometric_sup`,
+    `perfect_set`, `perfectTP`, and `perfect_set2`.
 ### Renamed
+- in file `topology.v` -> `separation_axioms.v`
+  + `totally_disconnected_cvg` -> `zero_dimensional_cvg`.
+
 
 ### Generalized
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 847b22641..bc3fe9f1c 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -118,7 +118,6 @@ Proof.
 by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->.
 Qed.
 
-
 Lemma compact_cluster_set1 (x : T) F V :
   hausdorff_space -> compact V -> nbhs x V ->
   ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
@@ -234,7 +233,6 @@ move=> npzq; exists (`]-oo, q[, `]p, +oo[)%classic; split => //=.
   by apply: npzq; exists r; rewrite rz zr.
 Qed.
 
-
 Section ball_hausdorff.
 Variables (R : numDomainType) (T : pseudoMetricType R).
 
@@ -329,8 +327,6 @@ Proof. by rewrite -closeE //; apply: cvg_close. Qed.
 Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
   {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
 Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
-
-
 End separated_topologicalType.
 
 Section separated_ptopologicalType.
@@ -370,7 +366,6 @@ Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
 Proof.
 move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
 Qed.
-
 End separated_ptopologicalType.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
@@ -411,7 +406,6 @@ apply/xsectionP; apply: (entourage_split x) => //.
 by have := cxy _ (entourage_inv (entourage_split_ent entA)).
 Qed.
 
-
 Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
   F --> l <-> ([cvg F in U] /\ close (lim F) l).
 Proof.
@@ -488,8 +482,6 @@ Local Close Scope relation_scope.
 
 #[global] Hint Resolve uniform_regular : core.
 
-
-
 Section totally_disconnected.
 Implicit Types T : topologicalType.
 
@@ -574,6 +566,7 @@ exists V; split; first split.
 Qed.
 
 End totally_disconnected.
+
 (* This section proves that uniform spaces, with a countable base for their
    entourage, are metrizable. The definition of this metric is rather arcane,
    and the proof is tough. That's ok because the resulting metric is not
@@ -901,7 +894,6 @@ Qed.
 
 End countable_uniform.
 
-
 Module Exports. HB.reexport. End Exports.
 End countable_uniform.
 Export countable_uniform.Exports.
@@ -929,7 +921,6 @@ HB.instance Definition _ : PseudoMetric R S :=
 
 End sup_pseudometric.
 
-
 Module gauge.
 Section gauge.
 Local Open Scope relation_scope.
@@ -1057,4 +1048,4 @@ move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
 by move=> y [] ? [->] -> /eqP.
 Qed.
 
-End perfect_sets.
\ No newline at end of file
+End perfect_sets.

From 6d988378769c75c526c8040fcbed95213d2b1d9f Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Thu, 3 Oct 2024 23:41:17 -0400
Subject: [PATCH 3/7] trying ot fix import statement

---
 theories/function_spaces.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index fcc1a68e8..2090e1479 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-Require Import reals signed topology separation_axioms.
+
+From mathcomp Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)

From 9714276b1e7476fcca39684deec960c380f64d6d Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Fri, 4 Oct 2024 10:43:44 -0400
Subject: [PATCH 4/7] fixing build

---
 theories/Make              | 1 +
 theories/function_spaces.v | 1 -
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Make b/theories/Make
index 9dfe5bd5f..26289e19d 100644
--- a/theories/Make
+++ b/theories/Make
@@ -13,6 +13,7 @@ reals.v
 landau.v
 Rstruct.v
 topology.v
+separation_axioms.v
 function_spaces.v
 cantor.v
 prodnormedzmodule.v
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index 2090e1479..05cc4d0c8 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,6 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-
 From mathcomp Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)

From 258e3e65e4b4a189882159c6093404c33ec57d4d Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 6 Oct 2024 23:59:26 +0900
Subject: [PATCH 5/7] fixes

---
 theories/derive.v            |  1 -
 theories/separation_axioms.v | 34 ++++++++++++++++++----------------
 theories/topology.v          |  4 ++--
 3 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/theories/derive.v b/theories/derive.v
index bb68f56c8..9f97fe633 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -3,7 +3,6 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
-Require Import separation_axioms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index bc3fe9f1c..1e20e9972 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -1,12 +1,11 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-From mathcomp Require Import filter reals signed topology.
-From mathcomp Require Export topology.
+Require Import filter reals signed.
+Require Export topology.
 
 (**md**************************************************************************)
 (* # Separation Axioms                                                        *)
@@ -17,7 +16,10 @@ From mathcomp Require Export topology.
 (* accessible, uniform, etc). This file also provides related topological     *)
 (* properties like zero dimensional and perfect, and discrete.                *)
 (*                                                                            *)
-(*              set_nbhs A == filter from open sets containing A              *)    
+(* ```                                                                        *)
+(*              set_nbhs A == filter from open sets containing A              *)
+(* ```                                                                        *)
+(*                                                                            *)
 (* ## The classic separation axioms                                           *)
 (* ```                                                                        *)
 (*      kolmogorov_space T == T is a Kolmogorov space (T0)                    *)
@@ -47,7 +49,6 @@ From mathcomp Require Export topology.
 (*                            of countably many pseudoMetrics                 *)
 (******************************************************************************)
 
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -97,7 +98,6 @@ End set_nbhs.
 Section point_separation_axioms.
 Context {T : topologicalType}.
 
-
 Definition accessible_space := forall x y, x != y ->
   exists A : set T, open A /\ x \in A /\ y \in ~` A.
 
@@ -174,7 +174,7 @@ rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //.
 by rewrite inE; apply: VUc; rewrite -inE.
 Qed.
 
-Lemma accessible_closed_set1 : accessible_space -> forall (x : T), closed [set x].
+Lemma accessible_closed_set1 : accessible_space -> forall x : T, 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]]].
@@ -317,7 +317,6 @@ Qed.
 Lemma close_eq x y : close x y -> x = y.
 Proof. by rewrite closeE. Qed.
 
-
 Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
 Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
 
@@ -378,7 +377,9 @@ Arguments close_cvg {T} F1 F2 {FF2} _.
 
 Section close_uniform.
 Implicit Types (U : uniformType).
-Lemma entourage_close {U} (x y : U) : close x y = forall A, entourage A -> A (x, y).
+
+Lemma entourage_close {U} (x y : U) :
+  close x y = forall A, entourage A -> A (x, y).
 Proof.
 rewrite propeqE; split=> [cxy A entA|cxy].
   have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy.
@@ -406,7 +407,8 @@ apply/xsectionP; apply: (entourage_split x) => //.
 by have := cxy _ (entourage_inv (entourage_split_ent entA)).
 Qed.
 
-Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
+Lemma cvg_closeP {U : puniformType} (F : set_system U) (l : U) :
+    ProperFilter F ->
   F --> l <-> ([cvg F in U] /\ close (lim F) l).
 Proof.
 move=> FF; split=> [Fl|[cvF]Cl].
@@ -437,7 +439,7 @@ Definition normal_space :=
 Definition regular_space :=
   forall a : T, filter_from (nbhs a) closure --> a.
 
-Lemma compact_regular (x : T) V : hausdorff_space T -> compact V -> 
+Lemma compact_regular (x : T) V : hausdorff_space T -> compact V ->
   nbhs x V -> {for x, regular_space}.
 Proof.
 move=> sep cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //.
@@ -533,7 +535,7 @@ move=> /(_ _ _ setC (powerset_filter_from_filter PF))[].
 by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF.
 Qed.
 
-Lemma zero_dimensional_ray {d} {T : orderTopologicalType d} (x y : T) : 
+Lemma zero_dimensional_ray {d} {T : orderTopologicalType d} (x y : T) :
   (x < y)%O -> zero_dimensional T ->
   exists U, [/\ clopen U, U y , ~ U x & forall l r, U r -> ~ U l -> l < r]%O.
 Proof.
@@ -695,7 +697,7 @@ Local Definition step_ball x e z := exists i, (n_step_ball i x e z).
 
 Local Lemma n_step_ball_pos n x e z : n_step_ball n x e z -> 0 < e.
 Proof.
-by case: n => [[]|] // n; case=> [?] [?] [?] [] ? ? ? ? <-; apply: addr_gt0.
+by case: n => [[]|] // n; case=> [?] [?] [?] [] ? ? ? ? <-; exact: addr_gt0.
 Qed.
 
 Local Lemma step_ball_pos x e z : step_ball x e z -> 0 < e.
@@ -880,11 +882,11 @@ Definition type : Type := let _ := countableBase in let _ := entF in T.
 #[export] HB.instance Definition _ := Uniform.on type.
 #[export] HB.instance Definition _ := Uniform_isPseudoMetric.Build R type
   step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.
-#[export] HB.instance Definition _ {q : Pointed T} := Pointed.copy type (Pointed.Pack q).
+#[export] HB.instance Definition _ {q : Pointed T} :=
+  Pointed.copy type (Pointed.Pack q).
 
 Lemma countable_uniform_bounded (x y : T) :
-  let U := [the pseudoMetricType R of type]
-  in @ball _ U x 2 y.
+  let U := [the pseudoMetricType R of type] in @ball _ U x 2 y.
 Proof.
 rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
 rewrite [X in `|X|%N](_ : _ = 0) ?absz0//.
diff --git a/theories/topology.v b/theories/topology.v
index 9ee494677..b3a18a594 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-From mathcomp Require Import filter reals signed.
-From mathcomp Require Export filter.
+Require Import reals signed.
+Require Export filter.
 
 (**md**************************************************************************)
 (* # Basic topological notions                                                *)

From 804714fec799597354b60da25dbfda413b37f1aa Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 7 Oct 2024 00:14:47 +0900
Subject: [PATCH 6/7] fix

---
 theories/cantor.v          | 5 ++---
 theories/function_spaces.v | 2 +-
 theories/normedtype.v      | 1 -
 theories/topology.v        | 2 +-
 4 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index 5408b00d7..6706dd772 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -1,11 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
-From mathcomp Require Import reals signed topology function_spaces.
-From mathcomp Require Import separation_axioms.
-From HB Require Import structures.
+Require Import reals signed topology function_spaces separation_axioms.
 
 (**md**************************************************************************)
 (* # The Cantor Space and Applications                                        *)
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index 05cc4d0c8..fcc1a68e8 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-From mathcomp Require Import reals signed topology separation_axioms.
+Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 4bd8b27fc..ca1f9c395 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -6,7 +6,6 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
-Require Import separation_axioms.
 Require Export separation_axioms.
 
 (**md**************************************************************************)
diff --git a/theories/topology.v b/theories/topology.v
index b3a18a594..cf93fafac 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
+From mathcomp Require Export filter.
 Require Import reals signed.
-Require Export filter.
 
 (**md**************************************************************************)
 (* # Basic topological notions                                                *)

From 7c0a3f868aa43db8b9cb710c6e8875ac68d4e9d3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 7 Oct 2024 00:24:28 +0900
Subject: [PATCH 7/7] fix

---
 theories/separation_axioms.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 1e20e9972..f6a82482b 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -4,7 +4,8 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-Require Import filter reals signed.
+From mathcomp Require Import filter.
+Require Import reals signed.
 Require Export topology.
 
 (**md**************************************************************************)