quasiIso_comp — Mathlib

English

If φ: K → L and φ′: L → M are quasi-isomorphisms, then their composition φ ≫ φ′ is a quasi-isomorphism.

Русский

Если φ: K → L и φ′: L → M — квазиизоморфизмы, то их композиция φ ≫ φ′ является квазиизоморфизмом.

LaTeX

$$$\text{If } \varphi: K \to L, \ \varphi': L \to M \text{ are quasi-isomorphisms, then } \\ (\varphi \circ \varphi') \text{ is a quasi-isomorphism.}$$$

Lean4

instance quasiIso_comp (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i] [∀ i, M.HasHomology i]
    [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] : QuasiIso (φ ≫ φ') where

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