not_isRightDescent_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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