Coding 2024-02-05
All right. I don't have time to explain it, but, by following some suggestions online, I managed to prove that summing from a series with indices drawn from a set, the order that the indices are chosen doesn't matter.
:)
Only abstractly, and not with IEEE floats as the output, of course.
Anyway, with that, and a few other things I wrote, I'm most of the way towards being ready to work on the absolute convergence stuff again.
:)
Doesn't the focus on countable sets in the context of absolute convergence require some form of bijective mapping to the naturals, thereby rendering the whole detour to avoid imposing an ordering on the sets of indices pointless?
At least I got some experience wrangling Dafny.
Anyway, it's late and I'm tired.
Good night.