English
A T0 space is equivalent to the pairwise existence: for distinct x,y there exists an open U with x∈U xor y∈U.
Русский
T0-пространство эквивалентно парному существованию: для различных x,y существует открытое U с x∈U xor y∈U.
LaTeX
$$$T0Space X \iff Pairwise \ fun x y => \ Exists U, IsOpen U ∧ Xor'(x ∈ U)(y ∈ U).$$$
Lean4
theorem minimal_nonempty_open_subsingleton [T0Space X] {s : Set X} (hs : IsOpen s)
(hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen 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
· exact 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) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)
exact hyU (this.symm.subset hy).2
