English
If X is Normal and R0, then X is completely regular.
Русский
Если X нормальное и удовлетворяет R0, тогда X полностью регулярное.
LaTeX
$$$[NormalSpace X] \\land [R0Space X] \\Rightarrow [CompletelyRegularSpace X]$$$
Lean4
instance instCompletelyRegularSpace [NormalSpace X] [R0Space X] : CompletelyRegularSpace X :=
by
rw [completelyRegularSpace_iff]
intro x K hK hx
have cx : IsClosed (closure { x }) := isClosed_closure
have d : Disjoint (closure { x }) K := by
rw [Set.disjoint_iff]
intro a ⟨hax, haK⟩
exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)
let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_isClosed cx hK d
let g : X → I := fun x => ⟨f x, hficc x⟩
have cg : Continuous g := cf.subtype_mk hficc
have hgx : g x = 0 := Subtype.ext (hfx (subset_closure (mem_singleton x)))
have hgK : EqOn g 1 K := fun k hk => Subtype.ext (hfK hk)
exact ⟨g, cg, hgx, hgK⟩
