quasiIso_iff — Mathlib

English

A morphism f is a quasi-isomorphism if and only if it is a quasi-isomorphism at every index i.

Русский

Гомоморфизм f является квазиизоморфизмом тогда и только тогда, когда он квазиизоморфизм на каждом индексе i.

LaTeX

$$QuasiIso f \iff ∀ i, QuasiIsoAt f i$$

Lean4

theorem quasiIso_iff (f : K ⟶ L) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i] : QuasiIso f ↔ ∀ i, QuasiIsoAt f i :=
  ⟨fun h => h.quasiIsoAt, fun h => ⟨h⟩⟩

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