quasiIso_πTruncGE_iff

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.quasiIso_πTruncGE_iff

English

QuasiIso (K.πTruncGE n) iff K.IsGE n (version with integer index).

Русский

QuasiIso(K.πTruncGE n) эквивалентно K.IsGE(n).

LaTeX

$$$ \\text{QuasiIso}(K.\\pi\\TruncGE(n)) \\Leftrightarrow K.IsGE(n) $$$

Lean4

theorem quasiIso_πTruncGE_iff : QuasiIso (K.πTruncGE n) ↔ K.IsGE n :=
  quasiIso_πTruncGE_iff_isSupported K (embeddingUpIntGE n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru