instIsStrictlyGEObjIntSingleFunctor

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.instIsStrictlyGEObjIntSingleFunctor

← MathLib Explorer

English

If K IsLE at n, then QuasiIso (K.ιTruncLE n).

Русский

Если K IsLE в n, то QuasiIso(K.ιTruncLE n).

LaTeX

$$$ [K.IsLE(n)] \\Rightarrow \\text{QuasiIso}(K.\\iTruncLE(n)) $$$

Lean4

instance [HasZeroObject C] (A : C) (n : ℤ) : ((singleFunctor C n).obj A).IsStrictlyGE n :=
  inferInstanceAs (IsStrictlyGE ((single C (ComplexShape.up ℤ) n).obj A) n)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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