isRightDescent_inv_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isRightDescent_inv_iff {w : W} {i : B} : cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i := by
  simpa using (cs.isLeftDescent_inv_iff (w := w⁻¹)).symm

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