IsGE — Mathlib

English

IsGE(X, n) means that X lies to the right of or at degree n with respect to the canonical t-structure on the derived category.

Русский

IsGE(X, n) означает, что X расположен справа от или на степени n относительно канонической t-структуры в производной категории.

LaTeX

$$$$ \text{IsGE}(X, n) \equiv T\text{Structure}.t.IsGE(X, n). $$$$

Lean4

/-- Given `X : DerivedCategory C` and `n : ℤ`, this property means
that `X` is `≥ n` for the canonical t-structure. -/
abbrev IsGE (X : DerivedCategory C) (n : ℤ) : Prop :=
  TStructure.t.IsGE X n

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