eq_comp_inv — Mathlib

English

Let α: X ≅ Y. For morphisms f: Z → Y and g: Z → X, we have g = f ≫ α.inv if and only if g ≫ α.hom = f.

Русский

Пусть α: X ≅ Y. Для морфизмов f: Z → Y и g: Z → X верно, что g = f ≫ α.inv тогда и только тогда, когда g ≫ α.hom = f.

LaTeX

$$$g = f \gg α.inv \;\Leftrightarrow\; g \gg α.hom = f$$$

Lean4

theorem eq_comp_inv (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = f ≫ α.inv ↔ g ≫ α.hom = f :=
  (comp_inv_eq α.symm).symm

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