normedSpace — Mathlib

English

Lp.simpleFunc E p μ forms a module over 𝕜 (with the given bounded scalar action).

Русский

Lp.simpleFunc E p μ образует модуль над 𝕜 с заданным действием скаляра.

LaTeX

$$$\\mathrm{Module}_{\\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 def normedSpace {𝕜} [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : NormedSpace 𝕜 (Lp.simpleFunc E p μ) :=
  ⟨norm_smul_le (α := 𝕜) (β := Lp.simpleFunc E p μ)⟩

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