sigmaFiniteSet

Stream: mathlib4

[Yury G. Kudryashov]

@Rémy Degenne The module docstring of the file about docs#MeasureTheory.Measure.toFinite says that sigmaFiniteSet is defined in this file, but you moved it to a new file in #14471

[Rémy Degenne]

Indeed, it looks like I forgot to update that. I probably wont have time to PR a change before a few days.

The definition toFinite and the results in that file were meant to be used in a future PR, but you improved some results about s-finite measures while I was making my sequence of PRs, so in the end I never used it for anything. I see that you have new results related to that in #16146. Feel free to change and/or delete things there.

[Yury G. Kudryashov]

I'm going to redefine toFinite using my new exists_... lemma.