trans_refl — Mathlib

English

For any α: X ≅ Y, the right unit with Iso.refl Y gives α, i.e., α ≪≫ Iso.refl Y = α.

Русский

Для любого α: X ≅ Y, правый единичный элемент вместе с Iso.refl Y даёт α: α ≪≫ Iso.refl Y = α.

LaTeX

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

Lean4

@[simp]
theorem trans_refl (α : X ≅ Y) : α ≪≫ Iso.refl Y = α := by ext; apply Category.comp_id

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