isBoundedSMul — Mathlib

English

On a normed space E, if 1 ≤ p, then 𝕜-scalar multiplication is bounded on Lp.simpleFunc E p μ.

Русский

На нормированном пространстве E, при 1 ≤ p, умножение на скаляр ограничено на Lp.simpleFunc E p μ.

LaTeX

$$$[Fact(1 \\le p)]\\Rightarrow \\mathrm{IsBoundedSMul}(\\,\\mathbb{K},\\, \\mathrm{Lp.simpleFunc}\\,E\\,p\\,\\mu)$$$

Lean4

/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a normed space. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral. -/
protected theorem isBoundedSMul [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 (Lp.simpleFunc E p μ) :=
  IsBoundedSMul.of_norm_smul_le fun r f => (norm_smul_le r (f : Lp E p μ) :)

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