IsLeftDescent

Mathlib.GroupTheory.Coxeter.Length

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.IsLeftDescent

← MathLib Explorer

English

The left descent of w by i is defined as ℓ(s_i w) < ℓ(w).

Русский

Левый спуск элемента w по индексу i определяется как ℓ(s_i w) < ℓ(w).

LaTeX

$$$$ IsLeftDescent(w,i) \equiv \ell(s_i w) < \ell(w) $$$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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