lift_inv_left_eq — Mathlib

English

Equality relating lift, f, g, h: lift (f ≫ ι) g ≫ μ = h if and only if g = lift f h ≫ μ.

Русский

Равенство, связывающее lift, f, g, h: 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_inv_left_eq [GrpObj B] (f g h : A ⟶ B) : lift (f ≫ ι) g ≫ μ = h ↔ g = lift f h ≫ μ := by
  rw [eq_comm, eq_lift_inv_left, eq_comm]

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