self_symm_id_assoc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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