isIso₂_of_shortExact_of_isIso₁₃'

English

Same statement as Iso₂_from_Isos but stated as an alternate formulation.

Русский

Та же самая формулировка, что и в Iso₂_from_Isos, но сформулирована иначе.

LaTeX

$$$ShortExact(S_1) \to ShortExact(S_2) \Rightarrow IsIso(\varphi.τ_2)$$$

Lean4

theorem isIso₂_of_shortExact_of_isIso₁₃' [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.ShortExact)
    (h₂ : S₂.ShortExact) (_ : IsIso φ.τ₁) (_ : IsIso φ.τ₃) : IsIso φ.τ₂ :=
  isIso₂_of_shortExact_of_isIso₁₃ φ h₁ h₂

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