IsLE

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

English

IsLE(n) means K is supported up to level n, i.e., K.IsSupported(embeddingUpIntLE n).

Русский

IsLE(n) означает, что K поддержан до уровня n, то есть K.IsSupported(embeddingUpIntLE n).

LaTeX

$$$K.IsLE(n) \coloneqq K.IsSupported(\mathrm{embeddingUpIntLE}(n))$$$

Lean4

/-- The condition that a cochain complex `K` is (cohomologically) `≤ n`. -/
abbrev IsLE (n : ℤ) :=
  K.IsSupported (embeddingUpIntLE n)

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

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

Разделы

Аффилиация

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