smul — Mathlib

English

If hf : MemHolder r f, then MemHolder r (c • f) for any scalar c in a suitable normed space.

Русский

Если hf: MemHolder r f, то MemHolder r (c • f) для любого скалярного множителя c в подходящем нормированном пространстве.

LaTeX

$$$\operatorname{MemHolder}(r,f) \Rightarrow \operatorname{MemHolder}(r, c\cdot f).$$$

Lean4

theorem smul {𝕜} [SeminormedRing 𝕜] [Module 𝕜 Y] [IsBoundedSMul 𝕜 Y] {c : 𝕜} (hf : MemHolder r f) :
    MemHolder r (c • f) :=
  (hf.holderWith.smul c).memHolder

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