norm_nnqsmul — Mathlib

English

The norm is homogeneous of degree 1 with respect to nonnegative rational scalars: for any x in E and q≥0, ‖q x‖ = q ‖x‖.

Русский

Норма однородна по степени 1 в отношении неотрицательных рациональных скаляров: для любого x∈E и q∈ℚ_{\ge 0} верно ‖q x‖ = q ‖x‖.

LaTeX

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

Lean4

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

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