nnnorm_nnqsmul — Mathlib

English

The nonnegative norm is homogeneous of degree 1 with respect to nonnegative rational scalars: ‖q x‖₊ = q ‖x‖₊ for q≥0.

Русский

Неотрицательная норма однородна по тем же скалярам: ‖q x‖₊ = q ‖x‖₊.

LaTeX

$$$$ \\| q \\cdot x \\|_{+} = q \\cdot \\| x \\|_{+} \\quad (q \\in \\mathbb{Q}_{\\ge 0},\\ x \\in E). $$$$

Lean4

theorem nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by
  simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x

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