truncLE'_hasHomology

Mathlib.Algebra.Homology.Embedding.TruncLEHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.truncLE'.truncLE'_hasHomology

English

In the truncLE' setting, one obtains QuasiIsoAt in degree j under suitable hypotheses.

Русский

В настройке truncLE' получаем QuasiIsoAt в степени j при соответствующих предпосылках.

LaTeX

$$$ QuasiIsoAt\big(K.truncLE'ToRestriction e\big) j $$$

Lean4

instance truncLE'_hasHomology (i : ι) : (K.truncLE' e).HasHomology i :=
  inferInstanceAs ((K.op.truncGE' e.op).unop.HasHomology i)

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

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

Разделы

Аффилиация

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