nnnorm_smul_const — Mathlib

English

For a continuous map f: α → R and a vector b in β, the nn-norm of f·const b equals the product of nn-norms: ‖f·const α b‖₊ = ‖f‖₊ · ‖b‖₊.

Русский

Для отображения f: α→R и константного отображения, умноженного на вектор b, норма nnnorm равна произведению норм: ‖f·const α b‖₊ = ‖f‖₊ · ‖b‖₊.

LaTeX

$$‖f · const α b‖₊ = ‖f‖₊ · ‖b‖₊$$

Lean4

@[simp]
theorem nnnorm_smul_const {R β : Type*} [SeminormedAddCommGroup β] [SeminormedRing R] [Module R β] [NormSMulClass R β]
    (f : C(α, R)) (b : β) : ‖f • const α b‖₊ = ‖f‖₊ * ‖b‖₊ := by
  simp only [nnnorm_eq_iSup_nnnorm, smul_apply', const_apply, nnnorm_smul, iSup_mul]

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