length_mul_ge_length_sub_length — Mathlib

English

For any w1, w2 in W, the difference ℓ(w1) - ℓ(w2) is at most the length of the product ℓ(w1 w2).

Русский

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

LaTeX

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

Lean4

theorem length_mul_ge_length_sub_length (w₁ w₂ : W) : ℓ w₁ - ℓ w₂ ≤ ℓ(w₁ * w₂) := by
  simpa [Nat.sub_le_of_le_add] using cs.length_mul_le (w₁ * w₂) w₂⁻¹

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