eq_inv_comp — Mathlib

English

Let α: X ≅ Y be an isomorphism in a category. For morphisms f: X → Z and g: Y → Z, we have g = α.inv ≫ f if and only if α.hom ≫ g = f.

Русский

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

LaTeX

$$$g = α^{-1} \circ f \;\Leftrightarrow\; α.hom \circ g = f$$$

Lean4

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

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