From 8acab5152bab32d8cbf05e1939ab15d559e50f98 Mon Sep 17 00:00:00 2001
From: zstone1 <zstonex@gmail.com>
Date: Mon, 18 Mar 2024 03:40:45 -0400
Subject: [PATCH] Completely regular spaces (#1186)

* adding uniform completely regular
---
 CHANGELOG_UNRELEASED.md |  5 +++++
 theories/normedtype.v   | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7de783728..2af1a12c8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/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`, 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index e0f2f841f..eaff40cd7 100644
--- a/theories/normedtype.v
+++ b/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.