isLeftInversion_simple_iff_isLeftDescent

English

For any i, the right inversion of w with respect to the simple reflection s_i is equivalent to the right descent of w at i.

Русский

Для любого i правая инверсия w относительно простого отражения s_i эквивалентна правой десентности w по i.

LaTeX

$$$cs.IsRightInversion w (s i) \leftrightarrow cs.IsRightDescent w i$$$

Lean4

@[simp]
theorem isLeftInversion_simple_iff_isLeftDescent (w : W) (i : B) : cs.IsLeftInversion w (s i) ↔ cs.IsLeftDescent w i :=
  by simp [IsLeftInversion, IsLeftDescent, cs.isReflection_simple i]

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