# Topological Mathlib Pull Request

## Pull Request to Mathlib about the definition of regular_spaces and some basic propositions.

April 26, 2021 ◦ 2 min

◦

This PR changes the definition of regular_space, requesting only the t0_space condition, instead of the t1_space that was asked before.

```
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 = ⊥)
```

Due to that change, I also had to reformulate the proof of the lemma separed_regular in src/topology/uniform_space/separation.lean adding the T₀ condition. I have also defined the Uryson space, with their respective lemmas about the relations with T₂ and T₃, and, finally, prove the relation between the definition of t1_space from mathlib and the common definition with open sets.

```
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
```

If you want to see the original Pull Request at the Mathlib Repository you can do it here.