connectedComponents_lift_unique' — Mathlib

English

If two maps g1,g2: ConnectedComponents(α) → β agree on all representatives from α, then g1 = g2.

Русский

Если две отображения g1,g2: ConnectedComponents(α) → β согласуются на всех представителях компонент, то g1 = g2.

LaTeX

$$$g_1 = g_2 \quad\text{если}\quad g_1 \circ (\\iota) = g_2 \circ (\\iota)$$$

Lean4

theorem connectedComponents_lift_unique' {β : Sort*} {g₁ g₂ : ConnectedComponents α → β}
    (hg : g₁ ∘ ((↑) : α → ConnectedComponents α) = g₂ ∘ (↑)) : g₁ = g₂ :=
  ConnectedComponents.surjective_coe.injective_comp_right hg

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