isStrictlyGE_of_iso

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

English

If K ≅ L and K isStrictlyGE at n, then L isStrictlyGE at n.

Русский

Если K ≅ L и K strictly GE в уровне n, то L также GE в уровне n.

LaTeX

$$$ (K \\cong L) \\Rightarrow (K.IsStrictlyGE(n) \\Rightarrow L.IsStrictlyGE(n)) $$$

Lean4

theorem isStrictlyGE_of_iso (n : ℤ) [K.IsStrictlyGE n] : L.IsStrictlyGE n := by apply isStrictlySupported_of_iso e

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

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

Разделы

Аффилиация

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