quasiIsoAt_of_isIso — Mathlib

English

If f is an isomorphism, then QuasiIsoAt f i holds for every i, given homology exists.

Русский

Если f является изоморфизмом, то QuasiIsoAt f i выполняется для каждого i при условии существования гомологий.

LaTeX

$$QuasiIsoAt f i$$

Lean4

instance quasiIsoAt_of_isIso (f : K ⟶ L) [IsIso f] (i : ι) [K.HasHomology i] [L.HasHomology i] : QuasiIsoAt f i :=
  by
  rw [quasiIsoAt_iff]
  infer_instance

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