refl_trans — Mathlib

English

For any isomorphism α: X ≅ Y, the left unit Iso.refl X composed with α yields α, i.e., refl_X ≪≫ α = α.

Русский

Любой изоморфизм α: X ≅ Y удовлетворяет, что Iso.refl X ∘ α = α.

LaTeX

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

Lean4

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

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