norm_smul_const — Mathlib

English

The standard norm of f·const b equals the product of norms: ||f·const α b|| = ||f|| · ||b||.

Русский

Стандартная норма выражения f·const b равна произведению норм: ||f·const α b|| = ||f|| · ||b||.

LaTeX

$$$\|f \cdot \text{const }\alpha b\| = \|f\| \cdot \|b\|$$$

Lean4

@[simp]
theorem norm_smul_const {R β : Type*} [SeminormedAddCommGroup β] [SeminormedRing R] [Module R β] [NormSMulClass R β]
    (f : C(α, R)) (b : β) : ‖f • const α b‖ = ‖f‖ * ‖b‖ := by
  simp only [← coe_nnnorm, NNReal.coe_mul, nnnorm_smul_const]

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