English
The ∀i, B_i-valued PreLp space has a distinguished 𝕜-subalgebra consisting exactly of those elements with finite ∞-norm; this is lp B ∞.
Русский
Пространство PreLp с значениями в B_i имеет естественное 𝕜-подалгебраическое подп пространство, состоящее ровно из элементов с конечной ∞-нормой; это lp B ∞.
LaTeX
$$$\text{lpInftySubalgebra}(B) = \{ f\in \text{PreLp } B : \text{Mem}_{\ell^{\infty}}(f) ∞\}.$$$
Lean4
/-- The `𝕜`-subalgebra of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,
with extra structure. -/
def _root_.lpInftySubalgebra : Subalgebra 𝕜 (PreLp B) :=
{ lpInftySubring B with
carrier := {f | Memℓp f ∞}
algebraMap_mem' := algebraMap_memℓp_infty }
