isIso_leftHomologyMap'_of_isIso — Mathlib

English

If φ is an isomorphism, then leftHomologyMap' φ h1 h2 is an isomorphism.

Русский

Если φ — изоморфизм, то leftHomologyMap' φ h1 h2 является изоморфизмом.

LaTeX

$$IsIso (leftHomologyMap'(φ,h1,h2))$$

Lean4

instance isIso_leftHomologyMap'_of_isIso (φ : S₁ ⟶ S₂) [IsIso φ] (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    IsIso (leftHomologyMap' φ h₁ h₂) :=
  (inferInstance : IsIso (leftHomologyMapIso' (asIso φ) h₁ h₂).hom)

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