Completely regular spaces (#1186)

* adding uniform completely regular

CHANGELOG_UNRELEASED.md

@@ -11,6 +11,11 @@
   + lemma `ge0_integralZr`
 - file `function_spaces.v`
 
+- in file `normedtype.v`,
+  + new definition `completely_regular_space`.
+  + new lemmas `point_uniform_separator`, and 
+    `uniform_completely_regular`.
+
 ### Changed
 - moved from `topology.v` to `function_spaces.v`: `prod_topology`, 
     `product_topology_def`, `proj_continuous`, `dfwith_continuous`, 

theories/normedtype.v

@@ -46,6 +46,8 @@ Require Import ereal reals signed topology prodnormedzmodule function_spaces.
 (*                    Urysohn A B == a continuous function T -> [0,1] which   *)
 (*                                   separates A and B when                   *)
 (*                                   `uniform_separator A B`                  *)
+(*       completely_regular_space == a space where points and closed sets can *)
+(*                                   be separated by a function into R        *)
 (*          uniform_separator A B == there is a suitable uniform space and    *)
 (*                                   entourage separating A and B             *)
 (*                      nbhs_norm == neighborhoods defined by the norm        *)
@@ -3644,6 +3646,7 @@ Qed.
 
 End normal_uniform_separators.
 End Urysohn.
+
 Lemma uniform_separatorP {T : topologicalType} {R : realType} (A B : set T) :
   uniform_separator A B <->
   exists (f : T -> R), [/\ continuous f, range f `<=` `[0, 1],
@@ -3711,6 +3714,35 @@ Proof. exact: (normal_spaceP 0%N 1%N). Qed.
 
 End normalP.
 
+Section completely_regular.
+
+Definition completely_regular_space {R : realType} {T : topologicalType} :=
+  forall (a : T) (B : set T), closed B -> ~ B a -> exists f : T -> R, [/\
+    continuous f,
+    f a = 0 &
+    f @` B `<=` [set 1] ].
+
+Lemma point_uniform_separator {T : uniformType} (x : T) (B : set T) :
+  closed B -> ~ B x -> uniform_separator [set x] B.
+Proof.
+move=> clB nBx; have : open (~` B) by rewrite openC.
+rewrite openE => /(_ _ nBx); rewrite /interior /= -nbhs_entourageE.
+case=> E entE EnB.
+pose T' := [the pseudoMetricType Rdefinitions.R of gauge.type entE].
+exists (Uniform.class T); exists E; split => //; last by move => ?.
+by rewrite -subset0 => -[? w [/= [-> ? ?]]]; exact: (EnB w).
+Qed.
+
+Lemma uniform_completely_regular {R : realType} {T : uniformType} :
+   @completely_regular_space R T.
+Proof.
+move=> x B clB Bx.
+have /(@uniform_separatorP _ R) [f] := point_uniform_separator clB Bx.
+by case=> ? _; rewrite image_set1 => fx ?; exists f; split => //; exact: fx.
+Qed.
+
+End completely_regular.
+
 Section pseudometric_normal.
 
 Lemma uniform_regular {X : uniformType} : @regular_space X.