instHasHomology

Mathlib.Algebra.Homology.Embedding.TruncGEHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.truncGE.instHasHomology

English

For every i', the truncated complex K.truncGE e has homology in degree i'.

Русский

Для каждого i' комплекс K.truncGE e имеет гомологию в степени i'.

LaTeX

$$$(K.\mathrm{truncGE} e).\mathrm{HasHomology}\; i'$$$

Lean4

instance (i' : ι') : (K.truncGE e).HasHomology i' :=
  by
  dsimp [truncGE]
  infer_instance

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

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

Разделы

Аффилиация

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