English
Let X be a topological space that is Hausdorff and paracompact. Then X is normal; equivalently, for any two disjoint closed sets A and B in X, there exist disjoint open neighborhoods U and V with A ⊆ U and B ⊆ V.
Русский
Пусть X — топологическое пространство, являющееся хаусдорфовым и паракомпактным. Тогда X нормальное; эквивалентно тому, что для любых двух непересекающихся замкнутых множеств A и B в X существуют попарно непересекающиеся открытые окрестности U и V такие, что A ⊆ U, B ⊆ V.
LaTeX
$$$\text{T2Space}(X) \land \text{ParacompactSpace}(X) \Rightarrow \text{T4Space}(X)$$$
Lean4
/-- **Dieudonné's theorem**: a paracompact Hausdorff space is normal.
Formalization is based on the proof
at [ncatlab](https://ncatlab.org/nlab/show/paracompact+Hausdorff+spaces+are+normal). -/
instance (priority := 100) of_paracompactSpace_t2Space [T2Space X] [ParacompactSpace X] : T4Space X := by
-- First we show how to go from points to a set on one side.
have :
∀ s t : Set X,
IsClosed s →
(∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v :=
fun s t hs H ↦ by
/- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then
`⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/
choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with ⟨u', hu'o, hcov', hu'fin, hsub⟩
refine
⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl, hcov', ?_,
disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩
rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
refine fun i x hxt hxu ↦ absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)
exact fun y hyu hyv ↦
(huv i).le_bot
⟨hsub _ hyu, hyv⟩
-- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`.
refine { normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ }
rcases
this t { x } ht fun y hy ↦
(by
simp_rw [singleton_subset_iff]
exact t2_separation (hst.symm.ne_of_mem hy hx)) with
⟨v, u, hv, hu, htv, hxu, huv⟩
exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩
