mem_lp_const_smul — Mathlib

English

If the scalar action is bounded on each E i, then for any c in 𝕜 and any f in lp E p, the scalar multiple c • f lies again in lp E p.

Русский

Если скалярное действие ограничено на каждом E_i, то для любого c в 𝕜 и f в lp(E,p) произведение c•f снова принадлежит lp(E,p).

LaTeX

$$$\\forall c\\in 𝕜\\ ,\\forall f\\in lp E(p):\\ c\\cdot f\\in lp E(p)$$$

Lean4

theorem mem_lp_const_smul (c : 𝕜) (f : lp E p) : c • (f : PreLp E) ∈ lp E p :=
  (lp.memℓp f).const_smul c

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