toLp — Mathlib

English

If 𝕜 is a normed field and p≥1, then Lp.simpleFunc E p μ is a normed space.

Русский

Если 𝕜 нормированное поле и p≥1, то Lp.simpleFunc E p μ — нормированное пространство.

LaTeX

$$$[NormedField\\ 𝕜][Fact(1\\le p)]\\Rightarrow \\mathrm{NormedSpace}_{𝕜}(\\mathrm{Lp.simpleFunc}\\,E\\,p\\,\\mu)$$$

Lean4

/-- Construct the equivalence class `[f]` of a simple function `f` satisfying `MemLp`. -/
abbrev toLp (f : α →ₛ E) (hf : MemLp f p μ) : Lp.simpleFunc E p μ :=
  ⟨hf.toLp f, ⟨f, rfl⟩⟩

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