English
Given a continuous map f: α → β into a totally disconnected space β, there is a well-defined lift to the space of connected components, sending each component to the common image of all its points under f.
Русский
При непрерывном отображении f: α → β в полностью разобщимое пространство β существует корректное отображение на множество компонент связности, которое каждой компоненте α сопоставляет общее значение изображения f на этой компоненте.
LaTeX
$$$\exists \hat{f}: \mathrm{ConnectedComponents}(\alpha) \to \beta\quad\text{such that}\quad \hat{f}(\\pi(a)) = f(a) \quad(\\forall a \in \alpha),$ где \\pi: \alpha \to \mathrm{ConnectedComponents}(\alpha) \\text{копонирующий морфизм.}$$$
Lean4
/-- The lift to `connectedComponents α` of a continuous map from `α` to a totally disconnected space
-/
def connectedComponentsLift (h : Continuous f) : ConnectedComponents α → β := fun x =>
Quotient.liftOn' x f h.image_eq_of_connectedComponent_eq
