feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le`

[kex-y]

---

Used by #16882

[RemyDegenne]

Could summable_of_sum_range_le be also generalized in some way, such that the same lemma would work for both real and nnreal? If it gets complicated and you don't want to investigate too much no problem, we can also merge this PR first.

[kex-y]

I'm not sure what structure will work here. My instinct is to use tendsto_of_monotone but that requires a conditionally_complete_linear_order which ennreal does not satisfy

[RemyDegenne]

Yeah, ennreal looks different. I was only talking about real and nnreal. The PR looks good. I let you decide whether you merge as it is now or not. bors d+

[bors[bot]]

:v: JasonKYi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kex-y]

I tried a bit more but I can't find a nice form to state the theorem in so it's sufficiently general. I think I'll merge this for now.

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests