not_isLeftDescent_iff — Mathlib

English

Not IsLeftDescent w i is equivalent to ℓ(s_i w) = ℓ(w) + 1.

Русский

Не IsLeftDescent w i эквивалентно ℓ(s_i w) = ℓ(w) + 1.

LaTeX

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

Lean4

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

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