chore(topology/algebra/infinite_sum): small todo (#7994)
Generalize a lemma from `f : ℕ → ℝ` to `f : β → α`, with
```lean
[add_comm_group α] [topological_space α] [topological_add_group α] [t2_space α] [decidable_eq β]
```
This was marked as TODO after #6017/#6096.
