algebraMap_memℓp_infty — Mathlib

English

The image of any element k of 𝕜 under the algebra map into the product space lies in the ∞-normed subspace (finite ∞-norm).

Русский

Образ элемента k из 𝕜 под алгебраической связкой в произведение функций лежит в подпространстве ∞-нормы (с конечной ∞-нормой).

LaTeX

$$$\text{Mem}_{\ell^{\infty}}(\text{algebraMap }\mathbb{K}((i\mapsto B_i))\, k) \;.$$$

Lean4

theorem _root_.algebraMap_memℓp_infty (k : 𝕜) : Memℓp (algebraMap 𝕜 (∀ i, B i) k) ∞ :=
  by
  rw [Algebra.algebraMap_eq_smul_one]
  exact (one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)

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