isIso_of_isIsos — Mathlib

English

The hom₃ component of a composition equals the composition of hom₃ components.

Русский

Компонента hom₃ композиции равна композиции ее компонентов hom₃.

LaTeX

$$$\mathrm{comp}(f,g).hom_{3} = f.hom_{3} \circ g.hom_{3}$$$

Lean4

theorem isIso_of_isIsos {A B : Triangle C} (f : A ⟶ B) (h₁ : IsIso f.hom₁) (h₂ : IsIso f.hom₂) (h₃ : IsIso f.hom₃) :
    IsIso f :=
  by
  let e := Triangle.isoMk A B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃) (by simp) (by simp) (by simp)
  exact (inferInstance : IsIso e.hom)

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