totallyDisconnectedSpace_iff_connectedComponent_subsingleton

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)

Похожие утверждения