English
A space is totally disconnected if and only if every connected component is a subsingleton.
Русский
Пространство полностью раздельно тогда и только тогда, когда каждый связанный компонент является подмножество с единственным элементом.
LaTeX
$$TotallyDisconnectedSpace(\alpha) \iff ∀ x: \alpha, (connectedComponent x).Subsingleton$$
Lean4
/-- A space is totally disconnected iff its connected components are subsingletons. -/
theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
TotallyDisconnectedSpace α ↔ ∀ x : α, (connectedComponent x).Subsingleton :=
by
constructor
· intro h x
apply h.1
· exact subset_univ _
exact isPreconnected_connectedComponent
intro h; constructor
intro s s_sub hs
rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)
· exact subsingleton_empty
· exact (h x).anti (hs.subset_connectedComponent x_in)