English
In a T0 space, if s is open and any nonempty open t ⊆ s equals s, then s is a subsingleton.
Русский
В T0-пространстве, если s открыто и любая непустая открытая подсекция t ⊆ s равна s, то s — subsingleton.
LaTeX
$$$\text{IsOpen}(s) \land (\forall t\subseteq s, t\text{ Nonempty } \land t\text{ IsOpen } t \Rightarrow t=s) \Rightarrow s\text{ Subsingleton}$$$
Lean4
/-- Given a closed set `S` in a compact T₀ space, there is some `x ∈ S` such that `{x}` is
closed. -/
theorem exists_closed_singleton [T0Space X] [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) :
∃ x : X, x ∈ S ∧ IsClosed ({ x } : Set X) :=
by
obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne
rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩
exact ⟨x, Vsub (mem_singleton x), Vcls⟩
