quasiIsoAt_shortComplexTruncLE_g — Mathlib

English

For a degree i', the map g in K.shortComplexTruncLE e is a quasi-iso.

Русский

Для степени i' отображение g в K.shortComplexTruncLE e является квазиизоморфизмом.

LaTeX

$$$ QuasiIsoAt\big(K.shortComplexTruncLE e\).g\ i' $$$

Lean4

theorem quasiIsoAt_shortComplexTruncLE_g (i' : ι') (hi' : ∀ i, e.f i ≠ i') :
    QuasiIsoAt (K.shortComplexTruncLE e).g i' :=
  by
  rw [quasiIsoAt_iff_isIso_homologyMap]
  exact K.isIso_homologyMap_shortComplexTruncLE_g e i' hi'

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