cleaning up discrete topologies

classical/filter.v

@@ -1311,27 +1311,21 @@ Section PrincipalFilters.
 Definition principal_filter {X : Type} (x : X) : set_system X :=
   globally [set x].
 
-(** we introducing an alias for pointed types with principal filters *)
-Definition principal_filter_type (P : Type) : Type := P.
-HB.instance Definition _ (P : choiceType) :=
-  Choice.copy (principal_filter_type P) P.
-HB.instance Definition _ (P : pointedType) :=
-  Pointed.on (principal_filter_type P).
-HB.instance Definition _ (P : choiceType) :=
-  hasNbhs.Build (principal_filter_type P) principal_filter.
-HB.instance Definition _ (P : pointedType) :=
-  Filtered.on (principal_filter_type P).
-
 Lemma principal_filterP {X} (x : X) (W : set X) : principal_filter x W <-> W x.
 Proof. by split=> [|? ? ->]; [exact|]. Qed.
 
 Lemma principal_filter_proper {X} (x : X) : ProperFilter (principal_filter x).
 Proof. exact: globally_properfilter. Qed.
 
-HB.instance Definition _ := hasNbhs.Build bool principal_filter.
-
 End PrincipalFilters.
 
+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}.
+
 Section UltraFilters.
 
 Class UltraFilter T (F : set_system T) := {

theories/cantor.v

@@ -43,12 +43,12 @@ Import numFieldTopology.Exports.
 
 Local Open Scope classical_set_scope.
 
-Definition cantor_space :=
-  prod_topology (fun _ : nat => discrete_topology discrete_bool).
+Definition cantor_space := 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.
+HB.instance Definition _ {R: realType} : @PseudoMetric R _ := 
+  PseudoMetric.on cantor_space.
 
 Definition cantor_like (T : topologicalType) :=
   [/\ perfect_set [set: T],
@@ -58,20 +58,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 nat (fun _ : nat => bool) (fun=> setT) (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.
+by apply: hausdorff_product => ?; exact: discrete_hausdorff.
 Qed.
 
 Lemma cantor_zero_dimensional : zero_dimensional cantor_space.
 Proof.
-apply: zero_dimension_prod => _; apply: discrete_zero_dimension.
-exact: discrete_space_discrete.
+by apply: zero_dimension_prod => _; exact: discrete_zero_dimension.
 Qed.
 
 Lemma cantor_perfect : perfect_set [set: cantor_space].
@@ -86,7 +84,6 @@ split.
 - exact: cantor_zero_dimensional.
 Qed.
 
-
 (**md**************************************************************************)
 (* ## Part 1                                                                  *)
 (*                                                                            *)
@@ -102,13 +99,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 +118,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 +189,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 +288,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).
@@ -356,7 +349,7 @@ End TreeStructure.
 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).
@@ -368,20 +361,19 @@ HB.instance Definition _ {R : realType} (T : nat -> pointedType) :
    @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.
@@ -469,9 +461,11 @@ 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.saturate.
+
 Let embed_refine n (U : set T) (k : K n) :=
   (if pselect (projT1 k `&` U !=set0)
   then projT1 k
@@ -485,18 +479,12 @@ Proof.
 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 +523,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)))).

theories/separation_axioms.v

@@ -5,7 +5,7 @@ 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.
-Require Import reals signed.
+Require Import reals signed topology.
 Require Export topology.
 
 (**md**************************************************************************)
@@ -113,10 +113,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 ->
@@ -177,14 +173,14 @@ 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 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=> //.
+move=> T1 x y /T1 [A [oA xA yA]]; exists A; left; split=> //.
 by rewrite nbhsE inE; exists A => //; rewrite inE in xA.
 Qed.
 
@@ -496,12 +492,6 @@ 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.
-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.
@@ -1054,3 +1044,19 @@ by move=> y [] ? [->] -> /eqP.
 Qed.
 
 End perfect_sets.
+
+Section discrete_separation.
+Context {X : discreteTopologicalType}.
+
+Lemma discrete_hausdorff : hausdorff_space X.
+Proof.
+by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q))[x [] -> ->].
+Qed.
+
+Lemma discrete_zero_dimension : zero_dimensional X.
+Proof.
+move=> x y xny; exists [set x]; split => //; last exact/nesym/eqP.
+by split; [exact: discrete_open | exact: discrete_closed].
+Qed.
+
+End discrete_separation.

theories/sequences.v

@@ -1377,9 +1377,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.