`BookProof.ChapterRieszFischer.sum_single_mem_finSupport` (f : Ell2) (s : Finset ℕ) : (∑ i ∈ s, lp.single 2 i ((f : ℕ → ℝ) i)) ∈ FinSupport

Initializing...

`BookProof.ChapterRieszFischer.sum_single_mem_finSupport` (f : Ell2) (s : Finset ℕ) : (∑ i ∈ s, lp.single 2 i ((f : ℕ → ℝ) i)) ∈ FinSupport · Prove2Me