isLeftDescent_inv_iff — Mathlib

English

For any w ∈ W and i ∈ B, IsLeftDescent w^{-1} i is equivalent to IsRightDescent w i.

Русский

Для любого w ∈ W и i ∈ B условие IsLeftDescent w^{-1} i эквивалентно IsRightDescent w i.

LaTeX

$$$$ \\text{IsLeftDescent}(w^{-1}, i) \\;\\Leftrightarrow\\; \\text{IsRightDescent}(w, i). $$$$

Lean4

theorem isLeftDescent_inv_iff {w : W} {i : B} : cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i :=
  by
  unfold IsLeftDescent IsRightDescent
  nth_rw 1 [← length_inv]
  simp

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