connectedSpace_iff_clopen — Mathlib

English

A space is connected iff it is nonempty and every clopen subset is trivial.

Русский

Пространство связано тогда и только тогда, когда оно непусто и любые открыто-закрытые подмножества тривиальны.

LaTeX

$$ConnectedSpace α \iff Nonempty α ∧ ∀ s ⊆ α, IsClopen s → s = ∅ ∨ s = α$$

Lean4

theorem connectedSpace_iff_clopen : ConnectedSpace α ↔ Nonempty α ∧ ∀ s : Set α, IsClopen s → s = ∅ ∨ s = Set.univ := by
  rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ, preconnectedSpace_iff_clopen,
    Set.nonempty_iff_univ_nonempty]

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