length_mul_ge_length_sub_length' — Mathlib

English

Similarly, the difference in the opposite order is bounded: ℓ(w2) - ℓ(w1) ≤ ℓ(w1 w2).

Русский

Аналогично, разность в обратном порядке ограничена: ℓ(w2) - ℓ(w1) ≤ ℓ(w1 w2).

LaTeX

$$$\\\\ell(w_2) - \\\\ell(w_1) \\\\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, add_comm] using cs.length_mul_le w₁⁻¹ (w₁ * w₂)

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