instHasHomologyTruncLE

Mathlib.Algebra.Homology.Embedding.TruncLEHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instHasHomologyTruncLE

English

For each i, (K.truncLE' e).HasHomology i holds.

Русский

Для каждого i верно, что (K.truncLE' e).HasHomology i существует.

LaTeX

$$$ (K.truncLE' e).HasHomology i $$$

Lean4

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

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

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

Разделы

Аффилиация

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