exists_rightDescent_of_ne_one

Mathlib.GroupTheory.Coxeter.Length

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.exists_rightDescent_of_ne_one

← MathLib Explorer

English

If w ≠ e, there exists i ∈ B such that IsRightDescent w i.

Русский

Если w ≠ e, существует i ∈ B такое, что IsRightDescent w i.

LaTeX

$$$$ w \\neq e \\;\\Rightarrow\\; \\exists i \\in B,\\; \\ell(w \\cdot s_i) < \\ell(w). $$$$

Lean4

theorem exists_rightDescent_of_ne_one {w : W} (hw : w ≠ 1) : ∃ i : B, cs.IsRightDescent w i :=
  by
  simp only [← isLeftDescent_inv_iff]
  apply exists_leftDescent_of_ne_one
  simpa

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru