isRightDescent_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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