norm_mul_le — Mathlib

English

The norm is subadditive under group operation: norm(xy) ≤ norm(x) + norm(y).

Русский

Норма подаддитивна относительно группы: norm(xy) ≤ norm(x) + norm(y).

LaTeX

$$$$\\forall x,y: FreeGroup(\\\\alpha),\\\\; \\\\mathrm{norm}(x y) \\\\le \\\\mathrm{norm}(x) + \\\\mathrm{norm}(y).$$$$

Lean4

@[to_additive]
theorem norm_mul_le (x y : FreeGroup α) : norm (x * y) ≤ norm x + norm y :=
  calc
    norm (x * y) = norm (mk (x.toWord ++ y.toWord)) := by rw [← mul_mk, mk_toWord, mk_toWord]
    _ ≤ (x.toWord ++ y.toWord).length := norm_mk_le
    _ = norm x + norm y := List.length_append

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