connectedSpace_iff_connectedComponent

English

A connected space is precisely one in which each point has the whole space as its connected component.

Русский

Связанное пространство — это такое, что для каждой точки вся пространство является её связной компонентой.

LaTeX

$$$$IsConnected(\\alpha) \\iff ∀ x \\in \\alpha,\\ \\operatorname{connectedComponent}(x) = \\mathrm{univ}$$$$

Lean4

theorem connectedSpace_iff_connectedComponent : ConnectedSpace α ↔ ∃ x : α, connectedComponent x = univ :=
  by
  constructor
  · rintro ⟨⟨x⟩⟩
    exact ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩
  · rintro ⟨x, h⟩
    haveI : PreconnectedSpace α := ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
    exact ⟨⟨x⟩⟩

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