preconnectedSpace_iff_connectedComponent

English

A preconnected space is characterized by the fact that every point lies in the whole space as its connected component.

Русский

Предсвязное пространство характеризуется тем, что для каждой точки её связная компонента равна всему пространству.

LaTeX

$$$$\\forall x:\\alpha,\\ \\operatorname{connectedComponent}(x) = \\mathrm{univ}$$$$

Lean4

theorem preconnectedSpace_iff_connectedComponent : PreconnectedSpace α ↔ ∀ x : α, connectedComponent x = univ :=
  by
  constructor
  · intro h x
    exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)
  · intro h
    rcases isEmpty_or_nonempty α with hα | hα
    · exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩
    · exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩

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