feat(topology/separation): change regular_space definition, added t1_…

…characterisation and definition of Urysohn space (#7367)

This PR changes the definition of regular_space becouse the previous definition requests t1_space and it's posible to only require t0_space as a condition. Due to that change, we had to reformulate the prove of the lemma separed_regular in src/topology/uniform_space/separation.lean adding the t0 condition.
We've also define the Uryson space , with his respectives lemmas about the relation with `T_2` and `T_3`, and prove the relation between the definition of t1_space from mathlib and the common definition with open sets.



Co-authored-by: carloscaralps <78864605+carloscaralps@users.noreply.github.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/topology/separation.lean

@@ -150,6 +150,30 @@ instance subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p
 instance t1_space.t0_space [t1_space α] : t0_space α :=
 ⟨λ x y h, ⟨{z | z ≠ y}, is_open_ne, or.inl ⟨h, not_not_intro rfl⟩⟩⟩
 
+lemma t1_iff_exists_open : t1_space α ↔
+  ∀ (x y), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U) :=
+begin
+  split,
+  { introsI t1 x y hxy,
+    exact ⟨{y}ᶜ, is_open_compl_iff.mpr (t1_space.t1 y),
+            mem_compl_singleton_iff.mpr hxy,
+            not_not.mpr rfl⟩},
+  { intro h,
+    constructor,
+    intro x,
+    rw ← is_open_compl_iff,
+    have p : ⋃₀ {U : set α | (x ∉ U) ∧ (is_open U)} = {x}ᶜ,
+    { apply subset.antisymm; intros t ht,
+      { rcases ht with ⟨A, ⟨hxA, hA⟩, htA⟩,
+        rw [mem_compl_eq, mem_singleton_iff],
+        rintro rfl,
+        contradiction },
+      { obtain ⟨U, hU, hh⟩ := h t x (mem_compl_singleton_iff.mp ht),
+        exact ⟨U, ⟨hh.2, hU⟩, hh.1⟩}},
+    rw ← p,
+    exact is_open_sUnion (λ B hB, hB.2) }
+end
+
 lemma compl_singleton_mem_nhds [t1_space α] {x y : α} (h : y ≠ x) : {x}ᶜ ∈ 𝓝 y :=
 mem_nhds_sets is_open_compl_singleton $ by rwa [mem_compl_eq, mem_singleton_iff]
 
@@ -386,6 +410,20 @@ lemma tendsto_nhds_unique_of_eventually_eq [t2_space α] {f g : β → α} {l :
   a = b :=
 tendsto_nhds_unique (ha.congr' hfg) hb
 
+/-- A T2,5 space, also known as a Urysohn space, is a topological space
+  where for every pair `x ≠ y`, there are two open sets, with the intersection of clousures
+  empty, one containing `x` and the other `y` . -/
+class t2_5_space (α : Type u) [topological_space α]: Prop :=
+(t2_5 : ∀ x y  (h : x ≠ y), ∃ (U V: set α), is_open U ∧  is_open V ∧
+                                            closure U ∩ closure V = ∅ ∧ x ∈ U ∧ y ∈ V)
+
+@[priority 100] -- see Note [lower instance priority]
+instance t2_5_space.t2_space [t2_5_space α] : t2_space α :=
+⟨λ x y hxy,
+  let ⟨U, V, hU, hV, hUV, hh⟩ := t2_5_space.t2_5 x y hxy in
+  ⟨U, V, hU, hV, hh.1, hh.2, subset_eq_empty (powerset_mono.mpr
+    (closure_inter_subset_inter_closure U V) subset_closure) hUV⟩⟩
+
 section lim
 variables [t2_space α] {f : filter α}
 
@@ -694,9 +732,22 @@ section regularity
 /-- A T₃ space, also known as a regular space (although this condition sometimes
   omits T₂), is one in which for every closed `C` and `x ∉ C`, there exist
   disjoint open sets containing `x` and `C` respectively. -/
-class regular_space (α : Type u) [topological_space α] extends t1_space α : Prop :=
+class regular_space (α : Type u) [topological_space α] extends t0_space α : Prop :=
 (regular : ∀{s:set α} {a}, is_closed s → a ∉ s → ∃t, is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥)
 
+@[priority 100] -- see Note [lower instance priority]
+instance regular_space.t1_space [regular_space α] : t1_space α :=
+begin
+  rw t1_iff_exists_open,
+  intros x y hxy,
+  obtain ⟨U, hU, h⟩ := t0_space.t0 x y hxy,
+  cases h,
+  { exact ⟨U, hU, h⟩ },
+  { obtain ⟨R, hR, hh⟩ := regular_space.regular (is_closed_compl_iff.mpr hU) (not_not.mpr h.1),
+    obtain ⟨V, hV, hhh⟩ := mem_nhds_sets_iff.1 (filter.inf_principal_eq_bot.1 hh.2),
+    exact ⟨R, hR, hh.1 (mem_compl h.2), hV hhh.2⟩ }
+end
+
 lemma nhds_is_closed [regular_space α] {a : α} {s : set α} (h : s ∈ 𝓝 a) :
   ∃ t ∈ 𝓝 a, t ⊆ s ∧ is_closed t :=
 let ⟨s', h₁, h₂, h₃⟩ := mem_nhds_sets_iff.mp h in
@@ -733,6 +784,17 @@ let ⟨s, hs, hys, hxs⟩ := regular_space.regular is_closed_singleton
 ⟨v, s, hv, hs, hxv, singleton_subset_iff.1 hys,
 eq_empty_of_subset_empty $ λ z ⟨hzv, hzs⟩, htu ⟨hvt hzv, hsu hzs⟩⟩⟩
 
+@[priority 100] -- see Note [lower instance priority]
+instance regular_space.t2_5_space [regular_space α] : t2_5_space α :=
+⟨λ x y hxy,
+let ⟨U, V, hU, hV, hh_1, hh_2, hUV⟩ := t2_space.t2 x y hxy,
+  hxcV := not_not.mpr ((interior_maximal (subset_compl_iff_disjoint.mpr hUV) hU) hh_1),
+  ⟨R, hR, hh⟩ := regular_space.regular is_closed_closure (by rwa closure_eq_compl_interior_compl),
+  ⟨A, hA, hhh⟩ := mem_nhds_sets_iff.1 (filter.inf_principal_eq_bot.1 hh.2) in
+⟨A, V, hhh.1, hV, subset_eq_empty ((closure V).inter_subset_inter_left
+  (subset.trans (closure_minimal hA (is_closed_compl_iff.mpr hR)) (compl_subset_compl.mpr hh.1)))
+  (compl_inter_self (closure V)), hhh.2, hh_2⟩⟩
+
 variable {α}
 
 lemma disjoint_nested_nhds [regular_space α] {x y : α} (h : x ≠ y) :

src/topology/uniform_space/separation.lean

@@ -175,7 +175,8 @@ end
 
 @[priority 100] -- see Note [lower instance priority]
 instance separated_regular [separated_space α] : regular_space α :=
-{ regular := λs a hs ha,
+{ t0 := by { haveI := separated_iff_t2.mp ‹_›, exact t1_space.t0_space.t0 },
+  regular := λs a hs ha,
     have sᶜ ∈ 𝓝 a,
       from mem_nhds_sets hs.is_open_compl ha,
     have {p : α × α | p.1 = a → p.2 ∈ sᶜ} ∈ 𝓤 α,