lift_coe — Mathlib

English

The lift evaluated at the quotient representative equals the original map's value on the representative; i.e., c.lift f H (toQuotient x) = f x.

Русский

Лифтированное отображение на представителе квадрирования равно значению исходного отображения на этом представителе.

LaTeX

$$$c.lift f H (toQuotient x) = f x$$$

Lean4

/-- The diagram describing the universal property for quotients of monoids commutes. -/
@[to_additive (attr := simp) /-- The diagram describing the universal property for quotients of
    `AddMonoid`s commutes. -/
    ]
theorem lift_coe (H : c ≤ ker f) (x : M) : c.lift f H x = f x :=
  rfl

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