IsStrictlyGE — Mathlib

English

The property IsStrictlyGE(n) means that K is strictly supported below n; equivalently, all components K.X_i vanish for i < n.

Русский

Свойство IsStrictlyGE(n) означает, что K поддержан строго ниже n; эквивалентно тому, что все компоненты K.X_i равны нулю для i < n.

LaTeX

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

Lean4

/-- The condition that a cochain complex `K` is strictly `≥ n`. -/
abbrev IsStrictlyGE (n : ℤ) :=
  K.IsStrictlySupported (embeddingUpIntGE n)

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