IsGE

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

English

IsGE(n) is the shorthand saying K is GE at level n, i.e., K.IsStrictlyGE(embeddingUpIntGE(n)).

Русский

IsGE(n) означает, что K ге по уровню n, то есть K.IsStrictlyGE(embeddingUpIntGE(n)).

LaTeX

$$$K.IsGE(n) \coloneqq K.IsStrictlyGE(\mathrm{embeddingUpIntGE}(n))$$$

Lean4

/-- The condition that a cochain complex `K` is (cohomologically) `≥ n`. -/
abbrev IsGE (n : ℤ) :=
  K.IsSupported (embeddingUpIntGE n)

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

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

Разделы

Аффилиация

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