From 67536afadf09946327cc04157060bc713c035a8a Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 28 Oct 2024 23:50:23 -0400
Subject: [PATCH] able to separate the discrete stuff more cleanly

---
 CHANGELOG_UNRELEASED.md                       |  18 ++
 _CoqProject                                   |   1 +
 theories/Make                                 |   1 +
 theories/cantor.v                             |  54 +++--
 theories/separation_axioms.v                  |  15 +-
 theories/sequences.v                          |   4 +-
 theories/topology_theory/bool_topology.v      |  26 +--
 theories/topology_theory/discrete_topology.v  | 197 ++++++++++++++++++
 theories/topology_theory/nat_topology.v       |  67 ++----
 .../topology_theory/pseudometric_structure.v  |  95 ---------
 theories/topology_theory/topology.v           |   1 +
 theories/topology_theory/topology_structure.v |  41 ----
 12 files changed, 284 insertions(+), 236 deletions(-)
 create mode 100644 theories/topology_theory/discrete_topology.v

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 03c90f7b0..c9ee51f7c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -57,6 +57,9 @@
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
 
+- in file `bool_topology.v`,
+  + new lemma `bool_compact`.
+
 ### Changed
 
 - in file `normedtype.v`,
@@ -74,6 +77,16 @@
     `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
     `disj_itv_Rhull`
 
+- moved from `topology_structure.v` to `discrete_topology.v`: 
+  `discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`.
+
+- moved from `pseudometric_structure.v` to `discrete_topology.v`:
+    `discrete_ent`, `discrete_ball`, and `discrete_topology`.
+
+- in file `cantor.v`, `cantor_space` now defined in terms of `bool`.
+- in file `separation_axioms.v`, updated `discrete_hausdorff`, and
+    `discrete_zero_dimension` to take a `discreteTopologicalType`.
+
 ### Renamed
 
 ### Generalized
@@ -82,6 +95,11 @@
 
 ### Removed
 
+- in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`.
+- in file `nat_topology.v`, removed `discrete_nat`.
+- in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and 
+    `discrete_space_discrete`.
+
 ### Infrastructure
 
 ### Misc
diff --git a/_CoqProject b/_CoqProject
index 0c3ff3b81..ffd88ff28 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -58,6 +58,7 @@ theories/topology_theory/weak_topology.v
 theories/topology_theory/num_topology.v
 theories/topology_theory/quotient_topology.v
 theories/topology_theory/one_point_compactification.v
+theories/topology_theory/discrete_topology.v
 
 theories/separation_axioms.v
 theories/function_spaces.v
diff --git a/theories/Make b/theories/Make
index 95312be86..5c5f465a1 100644
--- a/theories/Make
+++ b/theories/Make
@@ -26,6 +26,7 @@ topology_theory/weak_topology.v
 topology_theory/num_topology.v
 topology_theory/quotient_topology.v
 topology_theory/one_point_compactification.v
+topology_theory/discrete_topology.v
 separation_axioms.v
 function_spaces.v
 cantor.v
diff --git a/theories/cantor.v b/theories/cantor.v
index 8006e1ced..9fdac30dd 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -43,12 +43,13 @@ Import numFieldTopology.Exports.
 
 Local Open Scope classical_set_scope.
 
-Definition cantor_space :=
-  prod_topology (fun _ : nat => discrete_topology discrete_bool).
+Definition cantor_space : Type :=
+  prod_topology (fun _ : nat => bool).
 
 HB.instance Definition _ := Pointed.on cantor_space.
 HB.instance Definition _ := Nbhs.on cantor_space.
 HB.instance Definition _ := Topological.on cantor_space.
+HB.instance Definition _ := Uniform.on cantor_space.
 
 Definition cantor_like (T : topologicalType) :=
   [/\ perfect_set [set: T],
@@ -58,20 +59,18 @@ Definition cantor_like (T : topologicalType) :=
 
 Lemma cantor_space_compact : compact [set: cantor_space].
 Proof.
-have := @tychonoff _ (fun _ : nat => _) _ (fun=> discrete_bool_compact).
+have := @tychonoff _ (fun _ : nat => _) _ (fun=> bool_compact).
 by congr (compact _); rewrite eqEsubset.
 Qed.
 
 Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
 Proof.
 apply: hausdorff_product => ?; apply: discrete_hausdorff.
-exact: discrete_space_discrete.
 Qed.
 
 Lemma cantor_zero_dimensional : zero_dimensional cantor_space.
 Proof.
 apply: zero_dimension_prod => _; apply: discrete_zero_dimension.
-exact: discrete_space_discrete.
 Qed.
 
 Lemma cantor_perfect : perfect_set [set: cantor_space].
@@ -102,13 +101,12 @@ Qed.
 (*                                                                            *)
 (******************************************************************************)
 Section topological_trees.
-Context {K : nat -> ptopologicalType} {X : ptopologicalType}
+Context {K : nat -> pdiscreteTopologicalType} {X : ptopologicalType}
         (refine_apx : forall n, set X -> K n -> set X)
         (tree_invariant : set X -> Prop).
 
 Hypothesis cmptX : compact [set: X].
 Hypothesis hsdfX : hausdorff_space X.
-Hypothesis discreteK : forall n, discrete_space (K n).
 Hypothesis refine_cover : forall n U, U = \bigcup_e @refine_apx n U e.
 Hypothesis refine_invar : forall n U e,
   tree_invariant U -> tree_invariant (@refine_apx n U e).
@@ -122,7 +120,7 @@ Hypothesis refine_separates: forall x y : X, x != y ->
 Let refine_subset n U e : @refine_apx n U e `<=` U.
 Proof. by rewrite [X in _ `<=` X](refine_cover n); exact: bigcup_sup. Qed.
 
-Let T := prod_topology K.
+Let T := prod_topology (K : nat -> ptopologicalType).
 
 Local Fixpoint branch_apx (b : T) n :=
   if n is m.+1 then refine_apx (branch_apx b m) (b m) else [set: X].
@@ -193,7 +191,6 @@ near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
 move=> [->]; near: z; exists (proj n @^-1` [set b n]).
 split => //; suff : @open T (proj n @^-1` [set b n]) by [].
 apply: open_comp; [move=> + _; exact: proj_continuous| apply: discrete_open].
-exact: discreteK.
 Unshelve. all: end_near. Qed.
 
 Let apx_prefix b c n :
@@ -293,9 +290,7 @@ Local Lemma cantor_map : exists f : cantor_space -> T,
       set_surj [set: cantor_space] [set: T] f &
       set_inj [set: cantor_space] f ].
 Proof.
-have [] := @tree_map_props
-    (fun=> discrete_topology discrete_bool) T c_ind c_invar cmptT hsdfT.
-- by move=> ?; exact: discrete_space_discrete.
+have [] := @tree_map_props (fun=> bool) T c_ind c_invar cmptT hsdfT.
 - move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//].
   have [?|?] := pselect (U_ n `&` V !=set0 /\ ~` U_ n `&` V !=set0).
   + have [Unt|Unt] := pselect (U_ n t).
@@ -350,38 +345,40 @@ Qed.
 
 End TreeStructure.
 
+Section cantor.
+Context {R : realType}.
+
 (**md**************************************************************************)
 (* ## Part 3: Finitely branching trees are Cantor-like                        *)
 (******************************************************************************)
 Section FinitelyBranchingTrees.
 
 Definition tree_of (T : nat -> pointedType) : Type :=
-  prod_topology (fun n =>  discrete_topology_type (T n)).
+  prod_topology (fun n => discrete_topology (T n)).
 
 HB.instance Definition _ (T : nat -> pointedType) : Pointed (tree_of T):= 
   Pointed.on (tree_of T).
 
 HB.instance Definition _ (T : nat -> pointedType) := Uniform.on (tree_of T).
 
-HB.instance Definition _ {R : realType} (T : nat -> pointedType) : 
+HB.instance Definition _ (T : nat -> pointedType) : 
     @PseudoMetric R _ :=
    @PseudoMetric.on (tree_of T).
 
 Lemma cantor_like_finite_prod (T : nat -> ptopologicalType) :
-  (forall n, finite_set [set: discrete_topology_type (T n)]) ->
+  (forall n, finite_set [set: discrete_topology (T n)]) ->
   (forall n, (exists xy : T n * T n, xy.1 != xy.2)) ->
   cantor_like (tree_of T).
 Proof.
 move=> finiteT twoElems; split.
-- exact/(@perfect_diagonal (discrete_topology_type \o T))/twoElems.
+- exact/(@perfect_diagonal (discrete_topology \o T))/twoElems.
 - have := tychonoff (fun n => finite_compact (finiteT n)).
   set A := (X in compact X -> _).
   suff : A = [set: tree_of (fun x : nat => T x)] by move=> ->.
   by rewrite eqEsubset.
-- apply: (@hausdorff_product _ (discrete_topology_type \o T)) => n.
+- apply: (@hausdorff_product _ (discrete_topology \o T)) => n.
   by apply: discrete_hausdorff; exact: discrete_space_discrete.
 - apply: zero_dimension_prod => ?; apply: discrete_zero_dimension.
-  exact: discrete_space_discrete.
 Qed.
 
 End FinitelyBranchingTrees.
@@ -390,7 +387,7 @@ End FinitelyBranchingTrees.
 (* ## Part 4: Building a finitely branching tree to cover `T`                 *)
 (******************************************************************************)
 Section alexandroff_hausdorff.
-Context {R : realType} {T : pseudoPMetricType R}.
+Context {T : pseudoPMetricType R}.
 
 Hypothesis cptT : compact [set: T].
 Hypothesis hsdfT : hausdorff_space T.
@@ -469,9 +466,14 @@ HB.instance Definition _ n := gen_eqMixin (K' n).
 HB.instance Definition _ n := gen_choiceMixin (K' n).
 HB.instance Definition _ n := isPointed.Build (K' n) (K'p n).
 
-Let K n := K' n.
+Let K n := discrete_topology (K' n).
 Let Tree := @tree_of K.
 
+HB.instance Definition _ n :=
+  DiscreteTopology.on (K n). 
+HB.instance Definition _ n :=
+  Pointed.on (K n). 
+
 Let embed_refine n (U : set T) (k : K n) :=
   (if pselect (projT1 k `&` U !=set0)
   then projT1 k
@@ -486,17 +488,12 @@ case: e => W; have [//| _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
 exact.
 Qed.
 
-Let discrete_subproof (P : choiceType) :
-  discrete_space (principal_filter_type P).
-Proof. by []. Qed.
-
 Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T,
   continuous f & set_surj [set: Tree] [set: T] f.
 Proof.
 pose entn n := projT2 (cid (ent_balls' (count_unif n))).
-have [//| | |? []//| |? []// | |] := @tree_map_props
-    (discrete_topology_type \o K) T (embed_refine) (embed_invar) cptT hsdfT.
-- by move=> n; exact: discrete_space_discrete.
+have [ | |? []//| |? []// | |] := @tree_map_props
+    K T (embed_refine) (embed_invar) cptT hsdfT.
 - move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
   have [//|_ _ _ + _] := entn n; rewrite -subTset.
   move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.
@@ -535,7 +532,7 @@ Local Lemma cantor_surj_pt2 :
   exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
 Proof.
 have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
-apply: (@cantor_like_finite_prod (discrete_topology_type \o K)) => [n /=|n].
+apply: (@cantor_like_finite_prod (discrete_topology \o K)) => [n /=|n].
   have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
   suff -> : [set: {classic K' n}] =
       (@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
@@ -569,3 +566,4 @@ by exists f; rewrite -cstf; exact: cst_continuous.
 Qed.
 
 End alexandroff_hausdorff.
+End cantor.
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 4f54e83e1..cc5435258 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -111,11 +111,6 @@ 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.
@@ -211,6 +206,12 @@ move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ].
 by move=> ?; exists (P, Q); split => //=; [exact: oP | exact: oQ].
 Qed.
 
+Lemma discrete_hausdorff {T : discreteTopologicalType} : hausdorff_space T.
+Proof.
+by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->.
+Qed.
+
+
 Lemma order_hausdorff {d} {T : orderTopologicalType d} : hausdorff_space T.
 Proof.
 rewrite open_hausdorff=> p q; wlog : p q / (p < q)%O.
@@ -567,9 +568,9 @@ Definition totally_disconnected {T} (A : set T) :=
 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.
+Lemma discrete_zero_dimension {T : discreteTopologicalType} : zero_dimensional T.
 Proof.
-move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP.
+move=> x y xny; exists [set x]; split => //; last exact/nesym/eqP.
 by split; [exact: discrete_open | exact: discrete_closed].
 Qed.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index bbff8a624..06c2369b8 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1314,9 +1314,9 @@ Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) ->
   \forall n \near \oo, u n = 0%N.
 Proof.
 move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l].
-  by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1.
+  by rewrite nbhs_principalE.
 have /ul[b _ bul] : nbhs l [set l.-1; l].
-  by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1.
+  by rewrite nbhs_principalE ; apply/principal_filterP => /=; right.
 exists (maxn a b) => // n /= abn.
 rewrite (_ : u = fun n => nseries u n.+1 - nseries u n)%N; last first.
   by rewrite funeqE => i; rewrite /nseries big_nat_recr//= addnC addnK.
diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v
index 29b8dc62f..d31adde13 100644
--- a/theories/topology_theory/bool_topology.v
+++ b/theories/topology_theory/bool_topology.v
@@ -3,6 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_classical.
 From mathcomp Require Import signed reals topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure order_topology compact.
+From mathcomp Require Import discrete_topology.
 
 (**md**************************************************************************)
 (* # Topology for boolean numbers                                             *)
@@ -15,25 +16,19 @@ Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-HB.instance Definition _ := Nbhs_isNbhsTopological.Build bool
-  principal_filter_proper discrete_sing discrete_nbhs.
-
-Lemma discrete_bool : discrete_space bool.
-Proof. by []. Qed.
+HB.instance Definition _ := hasNbhs.Build bool principal_filter.
+HB.instance Definition _ := Discrete_ofNbhs.Build bool erefl.
+HB.instance Definition _ := DiscreteUniform_ofNbhs.Build bool.
 
 Lemma bool_compact : compact [set: bool].
 Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.
 
-Section bool_ord_topology.
-Local Open Scope classical_set_scope.
-Local Open Scope order_scope.
-
 Local Lemma bool_nbhs_itv (b : bool) :
   nbhs b = filter_from
     (fun i => itv_open_ends i /\ b \in i)
     (fun i => [set` i]).
 Proof.
-rewrite discrete_bool eqEsubset; split=> U; first last.
+rewrite nbhs_principalE eqEsubset; split=> U; first last.
   by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
 move/principal_filterP; case: b.
   move=> Ut; exists `]false, +oo[; first split => //; first by left.
@@ -43,12 +38,5 @@ by move=> r /=; rewrite in_itv /=; case: r.
 Qed.
 
 HB.instance Definition _ := Order_isNbhs.Build _ bool bool_nbhs_itv.
-End bool_ord_topology.
-
-Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool].
-Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.
-
-Definition pseudoMetric_bool {R : realType} :=
-  [the pseudoMetricType R of discrete_topology discrete_bool : Type].
-
-#[global] Hint Resolve discrete_bool : core.
+HB.instance Definition _ {R : numDomainType} := 
+  @DiscretePseudoMetric_ofUniform.Build R bool.
diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v
new file mode 100644
index 000000000..94e837eb8
--- /dev/null
+++ b/theories/topology_theory/discrete_topology.v
@@ -0,0 +1,197 @@
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals.
+From mathcomp Require Import topology_structure uniform_structure.
+From mathcomp Require Import order_topology pseudometric_structure compact.
+
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+
+HB.mixin Record Discrete_ofNbhs T of Nbhs T := {
+  nbhs_principalE : (@nbhs T _) = principal_filter;
+}.
+
+#[short(type="discreteNbhsType")]
+HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}.
+
+
+Definition discrete_ent {T} : set (set (T * T)) :=
+  globally (range (fun x => (x, x))).
+
+(** Note: having the discrete topology does not guarantee the discrete 
+    uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *)
+HB.mixin Record Discrete_ofUniform T of Uniform T := {
+  uniform_discrete : @entourage T = discrete_ent
+}.
+
+Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y.
+
+HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of 
+    PseudoMetric R T := {
+  metric_discrete : @ball R T = @discrete_ball R T
+}.
+
+#[short(type="discreteTopologicalType")]
+HB.structure Definition DiscreteTopology := 
+  { T of DiscreteNbhs T & Topological T}.
+
+#[short(type="discreteOrderTopologicalType")]
+HB.structure Definition DiscreteOrderTopology d := 
+  { T of Discrete_ofNbhs T & OrderTopological d T}.
+
+#[short(type="pdiscreteTopologicalType")]
+HB.structure Definition PointedDiscreteTopology := 
+  { T of DiscreteTopology T & Pointed T}.
+
+#[short(type="pdiscreteOrderTopologicalType")]
+HB.structure Definition PointedDiscreteOrderTopology d := 
+  { T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}.
+
+#[short(type="discreteUniformType")]
+HB.structure Definition DiscreteUniform := 
+  { T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}.
+
+#[short(type="discretePseudoMetricType")]
+HB.structure Definition DiscretePseudoMetric {R : numDomainType} := 
+  { T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.
+
+HB.builders Context T of Discrete_ofNbhs T.
+
+Local Lemma principal_nbhs_filter (p : T) : ProperFilter (nbhs p).
+Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed.
+
+Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
+Proof. by rewrite nbhs_principalE => /principal_filterP. Qed.
+
+Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A).
+Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed.
+
+HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T
+  principal_nbhs_filter principal_nbhs_singleton principal_nbhs_nbhs.
+
+HB.end.
+
+HB.factory Record DiscreteUniform_ofNbhs T of Discrete_ofNbhs T & Nbhs T := {}.
+HB.builders Context T of DiscreteUniform_ofNbhs T.
+
+Local Open Scope relation_scope.
+
+Local Notation d := (@discrete_ent T).
+
+Local Lemma discrete_entourage_filter : Filter d.
+Proof. exact: globally_filter. Qed.
+
+Local Lemma discrete_entourage_diagonal : forall A, d A -> diagonal `<=` A.
+Proof.
+by move=> ? + x x12; apply; exists x.1; rewrite // {2}x12 -surjective_pairing.
+Qed.
+
+Local Lemma discrete_entourage_inv : forall A, d A -> d A^-1.
+Proof. by move=> ? dA x [i _ <-]; apply: dA; exists i. Qed.
+
+Local Lemma discrete_entourage_split_ex :
+    forall A, d A -> exists2 B, d B & B \; B `<=` A.
+Proof.
+move=> ? dA; exists (range (fun x => (x, x))) => //.
+by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i.
+Qed.
+
+Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d.
+Proof.
+rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U.
+  move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. 
+  by move=> z /= /set_mem; rewrite /diagonal /= => <-.
+case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set.
+exact: entW.
+Qed.
+
+HB.instance Definition _ := @Nbhs_isUniform.Build T
+  discrete_ent 
+  discrete_entourage_filter 
+  discrete_entourage_diagonal 
+  discrete_entourage_inv
+  discrete_entourage_split_ex
+  discrete_entourage_nbhsE.
+
+HB.instance Definition _ := @Discrete_ofUniform.Build T erefl.
+
+HB.end.
+
+HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of 
+  DiscreteUniform T := {}.
+
+HB.builders Context R T of DiscretePseudoMetric_ofUniform R T.
+
+Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> 
+  @discrete_ball R T x eps x.
+Proof. by []. Qed.
+
+Local Lemma discrete_ball_sym (x y : T) (e : R) :
+  discrete_ball x e y -> discrete_ball y e x.
+Proof. by move=>->. Qed.
+Local Lemma discrete_ball_triangle (x y z:T) (e1 e2 : R) :
+  discrete_ball x e1 y -> discrete_ball y e2 z -> discrete_ball x (e1 + e2) z.
+Proof. by move=> -> ->. Qed.
+
+Local Lemma discrete_entourageE : entourage = entourage_ (@discrete_ball R T).
+Proof.
+rewrite predeqE => P; rewrite uniform_discrete; split; last first.
+  by move=> dbP ? [?] _ <-; move: dbP; case => /= ? ?; apply.
+move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
+by rewrite {2}z12 -surjective_pairing.
+Qed.
+
+HB.instance Definition _ := 
+  @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) 
+    discrete_ball_center discrete_ball_sym discrete_ball_triangle 
+    discrete_entourageE.
+
+Local Lemma discrete_ballE : @ball R T = @discrete_ball R T.
+Proof. by rewrite funeq2E => ? ?. Qed.
+
+HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE.
+
+HB.end.
+
+(** we introducing an alias attaching discrete structures for 
+    topology, uniformity, and pseudometric *)
+Definition discrete_topology (T : Type) : Type := T.
+HB.instance Definition _ (T : choiceType) :=
+  Choice.copy (discrete_topology T) T.
+HB.instance Definition _ (T : pointedType) :=
+  Pointed.on (discrete_topology T).
+HB.instance Definition _ (T : choiceType) :=
+  hasNbhs.Build (discrete_topology T) principal_filter.
+HB.instance Definition _ (T : choiceType) :=
+  Discrete_ofNbhs.Build (discrete_topology T) erefl.
+HB.instance Definition _ (T : choiceType) := 
+  DiscreteUniform_ofNbhs.Build (discrete_topology T).
+HB.instance Definition _ {R : numDomainType} (T : choiceType) := 
+  @DiscretePseudoMetric_ofUniform.Build R (discrete_topology T).
+
+Section discrete_topology.
+
+Context {X : discreteTopologicalType}.
+
+Lemma discrete_open (A : set X) : open A.
+Proof.
+rewrite openE => ? ?; rewrite /interior nbhs_principalE.
+exact/principal_filterP.
+Qed.
+
+Lemma discrete_set1 (x : X) : nbhs x [set x].
+Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed.
+
+Lemma discrete_closed (A : set X) : closed A.
+Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed.
+
+Lemma discrete_cvg (F : set_system X) (x : X) :
+  Filter F -> F --> x <-> F [set x].
+Proof.
+rewrite nbhs_principalE nbhs_simpl; split; first by exact.
+by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->.
+Qed.
+
+End discrete_topology.
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
index 4325ac634..0885f8c05 100644
--- a/theories/topology_theory/nat_topology.v
+++ b/theories/topology_theory/nat_topology.v
@@ -4,6 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import all_classical.
 From mathcomp Require Import signed reals topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure order_topology.
+From mathcomp Require Import discrete_topology.
 
 (**md**************************************************************************)
 (* # Topology for natural numbers                                             *)
@@ -16,20 +17,29 @@ Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Section nat_topologicalType.
+HB.instance Definition _ := hasNbhs.Build nat principal_filter.
+HB.instance Definition _ := Discrete_ofNbhs.Build nat erefl.
 
-Let D : set nat := setT.
-Let b : nat -> set nat := fun i => [set i].
-Let bT : \bigcup_(i in D) b i = setT.
-Proof. by rewrite predeqE => i; split => // _; exists i. Qed.
-
-Let bD : forall i j t, D i -> D j -> b i t -> b j t ->
-  exists k, [/\ D k, b k t & b k `<=` b i `&` b j].
-Proof. by move=> i j t _ _ -> ->; exists j. Qed.
-
-HB.instance Definition _ := isBaseTopological.Build nat bT bD.
+Local Lemma nat_nbhs_itv (n : nat) :
+  nbhs n = filter_from
+    (fun i => itv_open_ends i /\ n \in i)
+    (fun i => [set` i]).
+Proof.
+rewrite nbhs_principalE eqEsubset; split=> U; first last.
+  by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
+move/principal_filterP; case: n.
+  move=> U0; exists `]-oo, 1[; first split => //; first by left.
+  by move=> r /=; rewrite in_itv /=; case: r.
+move=> n USn; exists `]n, n.+2[; first split => //; first by right.
+  by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=.
+move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->.
+exact/esym/le_anti.
+Qed.
 
-End nat_topologicalType.
+HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv.
+HB.instance Definition _ := DiscreteUniform_ofNbhs.Build nat.
+HB.instance Definition _ {R : numDomainType} := 
+  @DiscretePseudoMetric_ofUniform.Build R nat.
 
 Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N.
 Proof. by exists N.+1. Qed.
@@ -102,6 +112,7 @@ by near: m; apply: AF; near: B; apply: nbhs_infty_ge.
 Unshelve. all: end_near. Qed.
 
 Section map.
+
 Context {I : Type} {F : set_system I} {FF : Filter F} (f : I -> nat).
 
 Lemma cvgnyPge :
@@ -123,35 +134,3 @@ Proof. exact: (cvgnyP 0%N 4%N). Qed.
 End map.
 
 End infty_nat.
-
-Lemma discrete_nat : discrete_space nat.
-Proof.
-rewrite /discrete_space predeq2E => n U; split.
-   by case => /= V [_ Vn VU]; exact/principal_filterP/VU.
-move/principal_filterP => Un; exists U; split => //=; exists U => //.
-by rewrite eqEsubset; split => [z [i Ui ->//]|z Uz]; exists z.
-Qed.
-
-Section nat_ord_topology.
-Local Open Scope classical_set_scope.
-Local Open Scope order_scope.
-
-Local Lemma nat_nbhs_itv (n : nat) :
-  nbhs n = filter_from
-    (fun i => itv_open_ends i /\ n \in i)
-    (fun i => [set` i]).
-Proof.
-rewrite discrete_nat eqEsubset; split=> U; first last.
-  by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb.
-move/principal_filterP; case: n.
-  move=> U0; exists `]-oo, 1[; first split => //; first by left.
-  by move=> r /=; rewrite in_itv /=; case: r.
-move=> n USn; exists `]n, n.+2[; first split => //; first by right.
-  by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=.
-move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->.
-exact/esym/le_anti.
-Qed.
-
-HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv.
-
-End nat_ord_topology.
diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v
index ec133325f..a88c1d2bd 100644
--- a/theories/topology_theory/pseudometric_structure.v
+++ b/theories/topology_theory/pseudometric_structure.v
@@ -19,19 +19,11 @@ From mathcomp Require Import signed reals topology_structure uniform_structure.
 (*                                   structure: a type equipped with balls    *)
 (*                                   The HB class is PseudoMetric.            *)
 (*              pseudoPMetricType == a pointed pseudoMetric space             *)
-(*         discrete_topology dscT == the discrete topology on T, provided     *)
-(*                                   dscT : discrete_space T                  *)
 (*                       ball x e == ball of center x and radius e            *)
 (*                nbhs_ball_ ball == nbhs defined using the given balls       *)
 (*                      nbhs_ball == nbhs defined using balls in a            *)
 (*                                   pseudometric space                       *)
-(*                   discrete_ent == entourages of the discrete uniformity    *)
-(*                                   topology                                 *)
-(*                  discrete_ball == singleton balls for the discrete metric  *)
-(*         discrete_topology_type == equip choice types with a discrete       *)
-(*                                   topology                                 *)
 (* ```                                                                        *)
-(* `discrete_ent` is equipped with the `Uniform` structure.                   *)
 (* ### Factories                                                              *)
 (* ```                                                                        *)
 (*            Nbhs_isPseudoMetric == factory to build a topological space     *)
@@ -89,37 +81,6 @@ HB.structure Definition PseudoMetric (R : numDomainType) :=
 HB.structure Definition PseudoPointedMetric (R : numDomainType) :=
   {T of Pointed T & Uniform T & Uniform_isPseudoMetric R T}.
 
-Definition discrete_topology T (dsc : discrete_space T) : Type := T.
-
-Section discrete_uniform.
-Context {T : nbhsType} {dsc: discrete_space T}.
-
-Definition discrete_ent : set (set (T * T)) :=
-  globally (range (fun x => (x, x))).
-
-Program Definition discrete_uniform_structure :=
-  @isUniform.Build (discrete_topology dsc) discrete_ent _ _ _ _.
-Next Obligation.
-by move=> ? + x x12; apply; exists x.1; rewrite // {2}x12 -surjective_pairing.
-Qed.
-Next Obligation.
-by move=> ? dA x [i _ <-]; apply: dA; exists i.
-Qed.
-Next Obligation.
-move=> ? dA; exists (range (fun x => (x, x))) => //.
-by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i.
-Qed.
-
-HB.instance Definition _ := Choice.on (discrete_topology dsc).
-HB.instance Definition _ := discrete_uniform_structure.
-End discrete_uniform.
-
-HB.instance Definition _ (P : pnbhsType) (dsc : discrete_space P) :=
-  Pointed.on (discrete_topology dsc).
-
-HB.instance Definition _ {T : pnbhsType} {dsc: discrete_space T} :=
-  Pointed.on (discrete_topology dsc).
-
 (* was uniformityOfBallMixin *)
 HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
   ent : set_system (M * M);
@@ -381,62 +342,6 @@ Qed.
 
 (** Specific pseudoMetric spaces *)
 
-Section discrete_pseudoMetric.
-Context {R : numDomainType} {T : nbhsType} {dsc : discrete_space T}.
-
-Definition discrete_ball (x : T) (eps : R) y : Prop := x = y.
-
-Lemma discrete_ball_center x (eps : R) : 0 < eps -> discrete_ball x eps x.
-Proof. by []. Qed.
-
-Program Definition discrete_pseudometric_structure :=
-  @Uniform_isPseudoMetric.Build R (discrete_topology dsc) discrete_ball
-    _ _ _ _.
-Next Obligation. by done. Qed.
-Next Obligation. by move=> ? ? ? ->. Qed.
-Next Obligation. by move=> ? ? ? ? ? -> ->. Qed.
-Next Obligation.
-rewrite predeqE => P; split; last first.
-  by case=> e _ leP; move=> [a b] [i _] [-> ->]; apply: leP.
-move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
-by rewrite {2}z12 -surjective_pairing.
-Qed.
-
-HB.instance Definition _ := discrete_pseudometric_structure.
-End discrete_pseudoMetric.
-
-(** we use `discrete_topology` to equip choice types with a discrete topology *)
-Section discrete_topology.
-
-Let discrete_subproof (P : choiceType) :
-  discrete_space (principal_filter_type P).
-Proof. by []. Qed.
-
-Definition discrete_topology_type (P : Type) : Type := P.
-
-HB.instance Definition _ (P : choiceType) := Choice.copy
-  (discrete_topology_type P) (discrete_topology (discrete_subproof P)).
-HB.instance Definition _ (P : choiceType) := Filtered.copy
-  (discrete_topology_type P) (discrete_topology (discrete_subproof P)).
-HB.instance Definition _  (P : choiceType) := Uniform.copy
-  (discrete_topology_type P) (discrete_topology (discrete_subproof P)).
-HB.instance Definition _ (P : pointedType) := Pointed.copy
-  (discrete_topology_type P) (discrete_topology (discrete_subproof P)).
-HB.instance Definition _ R (P : choiceType) : @PseudoMetric R _ :=
-  PseudoMetric.copy
-    (discrete_topology_type P) (discrete_topology (discrete_subproof P)).
-
-End discrete_topology.
-
-Lemma discrete_space_discrete (P : choiceType) :
-  discrete_space (discrete_topology_type P).
-Proof.
-apply/funext => /= x; apply/funext => A; apply/propext; split.
-- by move=> [E hE EA] _ ->; apply/EA/xsectionP/hE; exists x.
-- move=> h; exists diagonal; first by move=> -[a b] [t _] [<- <-].
-  by move=> y /xsectionP/= xy; exact: h.
-Qed.
-
 HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.
 
 Definition ball_
diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v
index 357618420..65e0ac9b0 100644
--- a/theories/topology_theory/topology.v
+++ b/theories/topology_theory/topology.v
@@ -15,3 +15,4 @@ From mathcomp Require Export topology_structure.
 From mathcomp Require Export uniform_structure.
 From mathcomp Require Export weak_topology.
 From mathcomp Require Export one_point_compactification.
+From mathcomp Require Export discrete_topology.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index 095ed1add..339813cc6 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -34,11 +34,6 @@ From mathcomp Require Export filter.
 (*                      x^' == set of neighbourhoods of x where x is          *)
 (*                             excluded (a "deleted neighborhood")            *)
 (*            limit_point E == the set of limit points of E                   *)
-(*         discrete_space T == every nbhs is a principal filter               *)
-(*                  dense S == the set (S : set T) is dense in T, with T of   *)
-(*                             type topologicalType                           *)
-(*      discrete_space dscT == the discrete topology on T, provided           *)
-(*                             a (dscT : discrete_space T)                    *)
 (*                                                                            *)
 (* ```                                                                        *)
 (* ### Factories                                                              *)
@@ -820,42 +815,6 @@ Qed.
 
 End closure_lemmas.
 
-Section DiscreteTopology.
-Section DiscreteMixin.
-Context {X : Type}.
-
-Lemma discrete_sing (p : X) (A : set X) : principal_filter p A -> A p.
-Proof. by move=> /principal_filterP. Qed.
-
-Lemma discrete_nbhs (p : X) (A : set X) :
-  principal_filter p A -> principal_filter p (principal_filter^~ A).
-Proof. by move=> ?; exact/principal_filterP. Qed.
-
-End DiscreteMixin.
-
-Definition discrete_space (X : nbhsType) := @nbhs X _ = @principal_filter X.
-
-Context {X : topologicalType} {dsc : discrete_space X}.
-
-Lemma discrete_open (A : set X) : open A.
-Proof.
-by rewrite openE => ? ?; rewrite /interior dsc; exact/principal_filterP.
-Qed.
-
-Lemma discrete_set1 (x : X) : nbhs x [set x].
-Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed.
-
-Lemma discrete_closed (A : set X) : closed A.
-Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed.
-
-Lemma discrete_cvg (F : set_system X) (x : X) :
-  Filter F -> F --> x <-> F [set x].
-Proof.
-rewrite dsc nbhs_simpl; split; first by exact.
-by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->.
-Qed.
-
-End DiscreteTopology.
 
 Definition dense (T : topologicalType) (S : set T) :=
   forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.