symm_self_id_assoc — Mathlib

English

For α: X ≅ Y and β: Y ≅ Z, α.symm.trans (α.trans β) = β.

Русский

Для α: X ≅ Y и β: Y ≅ Z, выполняется α.symm.trans (α.trans β) = β.

LaTeX

$$$\\forall {C} [\\mathrm{Category}(C)] {X Y Z} (\\alpha : X \\cong Y) (\\beta : Y \\cong Z), \\\\ alpha.symm.trans (alpha.trans beta) = beta$$$

Lean4

@[simp]
theorem symm_self_id_assoc (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪≫ β = β := by
  rw [← trans_assoc, symm_self_id, refl_trans]

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