connectedComponentsMap_continuous

English

If f is continuous, then the induced map on connected components is continuous.

Русский

Если отображение f непрерывно, то индуцированное отображение на компоненты связности также непрерывно.

LaTeX

$$$\text{Continuous}(h.\text{connectedComponentsMap})$$$

Lean4

theorem connectedComponentsMap_continuous {β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) :
    Continuous h.connectedComponentsMap :=
  Continuous.connectedComponentsLift_continuous (ConnectedComponents.continuous_coe.comp h)

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