English
A comprehensive equivalence (TFAE) of many characterizations of regular spaces holds: RegularSpace is equivalent to several related closure and neighborhood conditions.
Русский
Полное эквивалентное множество характеристик регулярного пространства: регулярность эквивалентна ряду условий про замыкания и окрестности.
LaTeX
$$$\\text{List.TFAE}([\\text{RegularSpace } X, \\ldots])$ expresses the equivalences among multiple formulations of regularity.$$
Lean4
theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
List.TFAE
[RegularSpace X, ∀ (s : Set X) x, x ∉ closure s → Disjoint (𝓝ˢ s) (𝓝 x),
∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s,
∀ (x : X) (s : Set X), s ∈ 𝓝 x → ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s, ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x,
∀ x : X, (𝓝 x).lift' closure = 𝓝 x] :=
by
tfae_have 1 ↔ 5 := by
rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap]
simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
(nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
(nhds_basis_opens _).disjoint_iff_right, ← subset_interior_iff_mem_nhdsSet, interior_compl, compl_subset_compl]
tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
tfae_have 6 → 4
| H, a, s, hs => by
rw [← H] at hs
rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
tfae_have 4 → 2
| H, s, a, ha => by
have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
tfae_have 2 → 3 :=
by
refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot
tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩
tfae_finish
