length_mul_simple — Mathlib

English

For any w1, w2 in W, max(ℓ(w1) - ℓ(w2), ℓ(w2) - ℓ(w1)) ≤ ℓ(w1 w2).

Русский

Для любых w1, w2 в W максимум между ℓ(w1) - ℓ(w2) и ℓ(w2) - ℓ(w1) не превосходит ℓ(w1 w2).

LaTeX

$$$$ \max(\\\\ell(w_1) - \\\\ell(w_2), \\\\ell(w_2) - \\\\ell(w_1)) \\\\le \\\\ell(w_1 w_2) $$$$

Lean4

theorem length_mul_simple (w : W) (i : B) : ℓ(w * s i) = ℓ w + 1 ∨ ℓ(w * s i) + 1 = ℓ w :=
  by
  rcases Nat.lt_or_gt_of_ne (cs.length_mul_simple_ne w i) with lt | gt
  · -- lt : ℓ (w * s i) < ℓ w

    right
    have length_ge := cs.length_mul_ge_length_sub_length w (s i)
    simp only [length_simple, tsub_le_iff_right] at length_ge
    cutsat
  · -- gt : ℓ w < ℓ (w * s i)

    left
    have length_le := cs.length_mul_le w (s i)
    simp only [length_simple] at length_le
    cutsat

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