IsLE — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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