`BookProof.ChapterEll2Separable.sum_single_rat_mem_range` (s : Finset ℕ) (q : ℕ → ℚ) : (∑ i ∈ s, lp.single 2 i ((q i : ℝ))) ∈ Set.range ratVec

Initializing...

`BookProof.ChapterEll2Separable.sum_single_rat_mem_range` (s : Finset ℕ) (q : ℕ → ℚ) : (∑ i ∈ s, lp.single 2 i ((q i : ℝ))) ∈ Set.range ratVec · Prove2Me