connectedComponentsLift_unique — Mathlib

English

If g is a map with g ∘ inclusion = f, then g equals the lift of f, i.e., g = h.connectedComponentsLift.

Русский

Если отображение g удовлетворяет g ∘ включение = f, то g совпадает с лифтом отображения f, то есть g = h.connectedComponentsLift.

LaTeX

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

Lean4

theorem connectedComponentsLift_unique (h : Continuous f) (g : ConnectedComponents α → β) (hg : g ∘ (↑) = f) :
    g = h.connectedComponentsLift :=
  connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm

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