English
The set of vector-valued functions whose lp-norm is finite, inside the pre-Lp space, forms a submodule; this is the lp E p itself endowed with the natural subspace structure.
Русский
Множество векторов-значений функций, чьи lp-нормы конечны, внутри пространства PreLp образует подмодуль; это пространство lp(E,p) наделено естественной структурой подпространства.
LaTeX
$$$lpSubmodule 𝕜 E p = \\{ f\\in PreLp E : \\|f\\|_{p}<\\infty\\}$ и является подпростра mod$$
Lean4
/-- The `𝕜`-submodule of elements of `∀ i : α, E i` whose `lp` norm is finite. This is `lp E p`,
with extra structure. -/
def _root_.lpSubmodule : Submodule 𝕜 (PreLp E) :=
{ lp E p with smul_mem' := fun c f hf => by simpa using mem_lp_const_smul c ⟨f, hf⟩ }
