instIsIsoIntιTruncLEOfIsStrictlyLE

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE

English

If K isLE at n, then the quasi-iso (K.πTruncGE n) holds in the LE sense, i.e., the truncation respects LE.

Русский

Если K имеет LE в n, то квазиизоморфизм (K.πTruncGE n) сохраняет LE.

LaTeX

$$$ (K.IsLE(n)) \\Rightarrow \\text{QuasiIso}(K.\\pi\\TruncGE(n)) $$$

Lean4

instance [K.IsStrictlyLE n] : IsIso (K.ιTruncLE n) := by dsimp [ιTruncLE]; infer_instance

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

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

Разделы

Аффилиация

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