lift_left_mul_ext — Mathlib

English

Another form of lift_inv_left_eq: lift (f ≫ ι) g ≫ μ = h if and only if g = lift f h ≫ μ.

Русский

Еще одна форма lift_inv_left_eq: lift (f ≫ ι) g ≫ μ = h тогда и только тогда, когда g = lift f h ≫ μ.

LaTeX

$$$\mathrm{lift}(f \circ \iota, g) \circ \mu = h \iff g = \mathrm{lift}(f, h) \circ \mu$$$

Lean4

theorem lift_left_mul_ext [GrpObj B] {f g : A ⟶ B} (i : A ⟶ B) (h : lift f i ≫ μ = lift g i ≫ μ) : f = g := by
  rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h

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