IsRightDescent — Mathlib

English

Let cs be a Coxeter system on W with generating set indexed by B. An element i ∈ B is a right descent of w ∈ W if the length ℓ(w s_i) is strictly less than ℓ(w).

Русский

Пусть cs — система Коксетера на группе W с базисом индексов B. Элемент i ∈ B является правым спадом элемента w ∈ W тогда и только тогда, когда длина ℓ(w s_i) строго меньше длины ℓ(w).

LaTeX

$$$$ \\ell(w \\cdot s_i) < \\ell(w). $$$$

Lean4

/-- The proposition that `i` is a right descent of `w`; that is, $\ell(w s_i) < \ell(w)$. -/
def IsRightDescent (w : W) (i : B) : Prop :=
  ℓ(w * s i) < ℓ w

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