length_mul_ge_max — Mathlib

English

For any w1, w2 in W, the maximum of the two differences is bounded by the length of the product: max(ℓ(w1) - ℓ(w2), ℓ(w2) - ℓ(w1)) ≤ ℓ(w1 w2).

Русский

Для любых w1, w2 в W максимум из двух разностей не превышает длину произведения: max(ℓ(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_ge_max (w₁ w₂ : W) : max (ℓ w₁ - ℓ w₂) (ℓ w₂ - ℓ w₁) ≤ ℓ(w₁ * w₂) :=
  max_le_iff.mpr ⟨length_mul_ge_length_sub_length _ _ _, length_mul_ge_length_sub_length' _ _ _⟩

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