isLeftDescent_iff — Mathlib

English

IsLeftDescent w i holds if and only if ℓ(s_i w) + 1 = ℓ(w).

Русский

IsLeftDescent w i выполняется тогда и только тогда, когда ℓ(s_i w) + 1 = ℓ(w).

LaTeX

$$$$ \\text{IsLeftDescent}(w,i) \\;\\Longleftrightarrow\\; \\ell(s_i \\cdot w) + 1 = \\ell(w). $$$$

Lean4

theorem isLeftDescent_iff {w : W} {i : B} : cs.IsLeftDescent w i ↔ ℓ(s i * w) + 1 = ℓ w :=
  by
  unfold IsLeftDescent
  constructor
  · intro _
    exact (cs.length_simple_mul w i).resolve_left (by cutsat)
  · cutsat

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