preconnectedSpace_iff_clopen — Mathlib

English

A space is preconnected iff every clopen subset is either empty or the whole space.

Русский

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

LaTeX

$$PreconnectedSpace α \iff ∀ s ⊆ α, IsClopen s → s = ∅ ∨ s = α$$

Lean4

theorem preconnectedSpace_iff_clopen : PreconnectedSpace α ↔ ∀ s : Set α, IsClopen s → s = ∅ ∨ s = Set.univ :=
  by
  refine ⟨fun _ _ => isClopen_iff.mp, fun h ↦ ?_⟩
  refine preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_
  have : f ⁻¹' { false } = (f ⁻¹' { true })ᶜ := by rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
  obtain (h | h) := h _ ((isClopen_discrete { true }).preimage hf) <;> simp_all

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