liftOfRightInverse_comp — Mathlib

English

If two lifts have the same defining data, they are equal.

Русский

Если две подъемные отображения заданы одними и теми же данными, они равны.

LaTeX

$$$ h = f.liftOfRightInverse f^{-1} hf ⟨g, hg⟩ \\Rightarrow h = f.liftOfRightInverse f^{-1} hf ⟨g, hg⟩ $$$

Lean4

@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp (hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) :
    (f.liftOfRightInverse f_inv hf g).comp f = g :=
  MonoidHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g

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