const_mul — Mathlib

English

If f has ℓ^p membership, then c • f is in ℓ^p for any c in a normed ring 𝕜 with module structure on each E_i.

Русский

Если f принадлежит ℓ^p, то c • f принадлежит ℓ^p для любого c в нормированном кольце 𝕜 с модульной структурой на каждом E_i.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(f,p) \Rightarrow \mathrm{Mem}_{\ell^p}(c \cdot f,p). $$$$

Lean4

theorem const_mul {f : α → 𝕜} (hf : Memℓp f p) (c : 𝕜) : Memℓp (fun x => c * f x) p :=
  hf.const_smul c

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