length_mul_le — Mathlib

English

For any w1, w2 in W, the length of the product is at most the sum of lengths: ℓ(w1 w2) ≤ ℓ(w1) + ℓ(w2).

Русский

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

LaTeX

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

Lean4

theorem length_mul_le (w₁ w₂ : W) : ℓ(w₁ * w₂) ≤ ℓ w₁ + ℓ w₂ :=
  by
  rcases cs.exists_reduced_word w₁ with ⟨ω₁, hω₁, rfl⟩
  rcases cs.exists_reduced_word w₂ with ⟨ω₂, hω₂, rfl⟩
  have := cs.length_wordProd_le (ω₁ ++ ω₂)
  simpa [hω₁, hω₂, wordProd_append] using this

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