English
If every point has an open neighborhood that is T0, then the whole space is T0.
Русский
Если каждому точке пространства соответствует открытое окрестности, которое является T0-пространством, то и само пространство является T0.
LaTeX
$$$(\\forall X)[TopologicalSpace X] \\\\left( \\forall x \\in X, \\exists s \\subseteq X, x \\in s \\land IsOpen(s) \\land T0Space(s)\\right) \\Rightarrow T0Space(X)$$$
Lean4
theorem of_cover (h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) : T0Space X :=
by
refine ⟨fun x y hxy => ?_⟩
rcases h x y hxy with ⟨s, hxs, hys, hs⟩
lift x to s using hxs; lift y to s using hys
rw [← subtype_inseparable_iff] at hxy
exact congr_arg Subtype.val hxy.eq
