preconnectedSpace_iff_univ — Mathlib

English

A topological space α is preconnected iff the universal set univ is preconnected.

Русский

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

LaTeX

$$$$PreconnectedSpace(\\alpha) \\iff IsPreconnected(\\mathrm{univ} : \\mathrm{Set}(\\alpha))$$$$

Lean4

theorem preconnectedSpace_iff_univ : PreconnectedSpace α ↔ IsPreconnected (univ : Set α) :=
  ⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

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