connectedSpace_iff_univ — Mathlib

English

A space α is connected iff the universal set univ is connected.

Русский

Пространство α связано тогда и только тогда, когда множество univ ⊆ α связано.

LaTeX

$$$$ConnectedSpace(\\alpha) \\iff IsConnected(\\mathrm{univ} : \\mathrm{Set}(\\alpha))$$$$

Lean4

theorem connectedSpace_iff_univ : ConnectedSpace α ↔ IsConnected (univ : Set α) :=
  ⟨fun h ↦ ⟨univ_nonempty, h.1.1⟩, fun h ↦ ConnectedSpace.mk (toPreconnectedSpace := ⟨h.2⟩) ⟨h.1.some⟩⟩

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