isGE_of_iso

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

English

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

Русский

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

LaTeX

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

Lean4

theorem isGE_of_iso (n : ℤ) [K.IsGE n] : L.IsGE n := by apply isSupported_of_iso e

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

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

Разделы

Аффилиация

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