lift_comp_mk' — Mathlib

English

The lift built from f and the quotient mk' composes with the quotient map to yield f on the original domain; i.e., (c.lift f H).comp c.mk' = f.

Русский

Лифт, построенный из f и mk' композитно срабатывает на исходном домене и даёт f: (c.lift f H).comp c.mk' = f.

LaTeX

$$$(c.lift f H).comp c.mk' = f$$$

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_comp_mk' (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f := by ext; rfl

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