lift_unique — Mathlib

English

The equivalence FreeGroup.lift is unique: given any two maps matching on generators, they are equal.

Русский

Единственность отображения lift: если оно совпадает на генераторах, то все совпадают.

LaTeX

$$$\\forall g,h:(FreeGroup(\\alpha)\\to_*\\beta),\\ \\ (\\forall a, g(of(a))=h(of(a))) \\Rightarrow g=h$$$

Lean4

@[to_additive]
theorem lift_unique (g : FreeGroup α →* β) (hg : ∀ x, g (FreeGroup.of x) = f x) {x} : g x = FreeGroup.lift f x :=
  DFunLike.congr_fun (lift.symm_apply_eq.mp (funext hg : g ∘ FreeGroup.of = f)) x

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