symm_self_id — Mathlib

English

For any α: X ≅ Y, the composition α.symm ≪≫ α is the identity on Y: α.symm ≪≫ α = Iso.refl Y.

Русский

Для любого α: X ≅ Y, композиция α.symm ≪≫ α является тождеством на Y: α.symm ≪≫ α = Iso.refl Y.

LaTeX

$$$\\forall {C} [\\mathrm{Category}(C)], {X Y} (\\alpha : X \\cong Y), \\ \\alpha.symm \\llbracket \\gg \\alpha = \\mathrm{Iso.refl}\\ Y$$$

Lean4

@[simp]
theorem symm_self_id (α : X ≅ Y) : α.symm ≪≫ α = Iso.refl Y :=
  ext α.inv_hom_id

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