comp_hom_eq_id — Mathlib

English

Let α: X ≅ Y, f: Z → Y, 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 comp_hom_eq_id (α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.hom = 𝟙 Y ↔ f = α.inv := by rw [← eq_comp_inv, id_comp]

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