lift_inv_right_eq — Mathlib

English

Equality describing lift with g and h: lift f (g ≫ ι) ≫ μ = h iff f = lift h g ≫ μ.

Русский

Равенство, описывающее lift с g и h: lift f (g ≫ ι) ≫ μ = h тогда и только тогда, когда f = lift h g ≫ μ.

LaTeX

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

Lean4

theorem lift_inv_right_eq [GrpObj B] (f g h : A ⟶ B) : lift f (g ≫ ι) ≫ μ = h ↔ f = lift h g ≫ μ := by
  rw [eq_comm, eq_lift_inv_right, eq_comm]

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