inv_hom_id_triangle_hom₃ — Mathlib

English

For an isomorphism e: A ≅ B of triangles, the inverse’s third component composed with the forward’s third component equals the identity on B's third object.

Русский

Для изоморфизма треугольников e: A ≅ B, композиция третьего компонента обратного с третьим компонентом прямого равна единице на B.obj3.

LaTeX

$$$e_{\text{inv},3} \circ e_{\text},3 = \mathrm{Id}_{B_3}$$$

Lean4

@[reassoc (attr := simp)]
theorem _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) :
    e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 _ := by rw [← comp_hom₃, e.inv_hom_id, id_hom₃]

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