hom_inv_id_triangle_hom₁ — Mathlib

English

Two triangle morphisms are equal if their three components are pairwise equal.

Русский

Два морфизма треугольника равны, если их три компонента равны попарно.

LaTeX

$$$\forall f,g:\,A\to B, \; f.hom_{i} = g.hom_{i} \; (i=1,2,3) \Rightarrow f = g$$$

Lean4

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

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