isIso₁_of_isIso₂₃ — Mathlib

English

If mor2 and mor3 are isomorphisms, mor1 is an isomorphism.

Русский

Если mor2 и mor3 изоморфизмы, mor1 изоморфизм.

LaTeX

$$$(T \\in \\mathrm{distTriang} \\, C) \\Rightarrow \\mathrm{IsIso}(T.mor_2) \\land \\mathrm{IsIso}(T.mor_3) \\Rightarrow \\mathrm{IsIso}(T.mor_1)$$$

Lean4

theorem isIso₁_of_isIso₂₃ {T T' : Triangle C} (φ : T ⟶ T') (hT : T ∈ distTriang C) (hT' : T' ∈ distTriang C)
    (h₂ : IsIso φ.hom₂) (h₃ : IsIso φ.hom₃) : IsIso φ.hom₁ :=
  isIso₂_of_isIso₁₃ ((invRotate C).map φ) (inv_rot_of_distTriang _ hT) (inv_rot_of_distTriang _ hT')
    (by dsimp; infer_instance) (by dsimp; infer_instance)

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