exists_leftDescent_of_ne_one — Mathlib

English

If w ≠ e (the identity), there exists i ∈ B such that IsLeftDescent w i.

Русский

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

LaTeX

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

Lean4

theorem exists_leftDescent_of_ne_one {w : W} (hw : w ≠ 1) : ∃ i : B, cs.IsLeftDescent w i :=
  by
  rcases cs.exists_reduced_word w with ⟨ω, h, rfl⟩
  have h₁ : ω ≠ [] := by rintro rfl; simp at hw
  rcases List.exists_cons_of_ne_nil h₁ with ⟨i, ω', rfl⟩
  use i
  rw [IsLeftDescent, ← h, wordProd_cons, simple_mul_simple_cancel_left]
  calc
    ℓ(π ω') ≤ ω'.length := cs.length_wordProd_le ω'
    _ < (i :: ω').length := by simp

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