hom_comp_eq_id — Mathlib

English

Let α: X ≅ Y be an isomorphism. For f: Y → X, we have α.hom ≫ f = 𝟙_X if and only if f = α.inv.

Русский

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

LaTeX

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

Lean4

theorem hom_comp_eq_id (α : X ≅ Y) {f : Y ⟶ X} : α.hom ≫ f = 𝟙 X ↔ f = α.inv := by rw [← eq_inv_comp, comp_id]

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