connectedComponentsLift_comp_coe — Mathlib

English

The lift composed with the canonical inclusion α → ConnectedComponents(α) equals the original map f, i.e., h.connectedComponentsLift ∘ (inclusion) = f.

Русский

Лифт, затем каноническое включение α → ConnectedComponents(α), равен исходному отображению f: α → β, то есть h.connectedComponentsLift ∘ incl = f.

LaTeX

$$$(h.\text{connectedComponentsLift}) \circ (\\iota) = f$$$

Lean4

@[simp]
theorem connectedComponentsLift_comp_coe (h : Continuous f) : h.connectedComponentsLift ∘ (↑) = f :=
  rfl

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