isRightDescent_iff_not_isRightDescent_mul

English

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

Русский

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

LaTeX

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

Lean4

theorem isRightDescent_iff_not_isRightDescent_mul {w : W} {i : B} :
    cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * s i) i :=
  by
  rw [isRightDescent_iff, not_isRightDescent_iff, simple_mul_simple_cancel_right]
  tauto

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