English
If f ∈ ℓ^p, then c•f ∈ ℓ^p for any scalar c, including more general scalar actions in modules.
Русский
Если f ∈ ℓ^p, то c·f ∈ ℓ^p для любого скаляра c, в контексте модулей.
LaTeX
$$$$ \mathrm{Mem}_{\ell^p}(f,p) \Rightarrow \mathrm{Mem}_{\ell^p}(c \cdot f,p). $$$$
Lean4
theorem finset_sum {ι} (s : Finset ι) {f : ι → ∀ i, E i} (hf : ∀ i ∈ s, Memℓp (f i) p) :
Memℓp (fun a => ∑ i ∈ s, f i a) p :=
by
haveI : DecidableEq ι := Classical.decEq _
revert hf
refine Finset.induction_on s ?_ ?_
· simp only [zero_mem_ℓp', Finset.sum_empty, imp_true_iff]
· intro i s his ih hf
simp only [his, Finset.sum_insert, not_false_iff]
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))
