English
A continuous map f: α → β induces a map on connected components, i.e., there exists a function from ConnectedComponents(α) to ConnectedComponents(β) making the diagram commute: F ∘ mk_α = mk_β ∘ f.
Русский
Непрерывное отображение f: α → β индуцирует отображение между компонентами связности: существует функция F: ConnectedComponents(α) → ConnectedComponents(β), такая что F ∘ mk_α = mk_β ∘ f.
LaTeX
$$$\exists F:\mathrm{ConnectedComponents}(\alpha) \to \mathrm{ConnectedComponents}(\beta),\quad F \circ \mathrm{mk}_α = \mathrm{mk}_β \circ f$$$
Lean4
/-- Functoriality of `connectedComponents` -/
def connectedComponentsMap {β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) :
ConnectedComponents α → ConnectedComponents β :=
Continuous.connectedComponentsLift (ConnectedComponents.continuous_coe.comp h)
