isLeftDescent_iff_not_isLeftDescent_mul

English

IsLeftDescent w i is equivalent to not IsLeftDescent (s_i w) i.

Русский

IsLeftDescent w i эквивалентно не IsLeftDescent (s_i w) i.

LaTeX

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

Lean4

theorem isLeftDescent_iff_not_isLeftDescent_mul {w : W} {i : B} :
    cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (s i * w) i :=
  by
  rw [isLeftDescent_iff, not_isLeftDescent_iff, simple_mul_simple_cancel_left]
  tauto

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