English
In a T0 space, if s is closed and any nonempty closed t ⊆ s equals s, then s is a subsingleton.
Русский
В T0-пространстве, если s замкнуто и любая непустая замкнутая подмножество t ⊆ s равна s, то s — подмножество с одним элементом.
LaTeX
$$$\text{IsClosed}(s) \land (\forall t\subseteq s, t\text{ Nonempty } \land t\text{ IsClosed } t \Rightarrow t=s) \Rightarrow s\text{ Subsingleton}$$$
Lean4
theorem minimal_nonempty_closed_subsingleton [T0Space X] {s : Set X} (hs : IsClosed s)
(hmin : ∀ t, t ⊆ s → t.Nonempty → IsClosed t → t = s) : s.Subsingleton :=
by
refine fun x hx y hy => of_not_not fun hxy => ?_
rcases exists_isOpen_xor'_mem hxy with ⟨U, hUo, hU⟩
wlog h : x ∈ U ∧ y ∉ U
· refine this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)
obtain ⟨hxU, hyU⟩ := h
have : s \ U = s := hmin (s \ U) diff_subset ⟨y, hy, hyU⟩ (hs.sdiff hUo)
exact (this.symm.subset hx).2 hxU
