Lusin

[zstone1]

Motivation for this change

Moving along with #965, this is lusin's theorem. The proof makes good use of the topology machinery from last year. Subspaces and restricted uniform convergence are useful here. And all the required lemmas were already done, and applied easily. So that's reassuring.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

measureU2 can be proved from the property of contents but generalizing the lemma from {measure _ -> _} to {content _ -> _} causes later rewrites to be ineffective.

[affeldt-aist]

measureU2 can be proved from the property of contents but generalizing the lemma from {measure _ -> _} to {content _ -> _} causes later rewrites to be ineffective.

This was actually no big deal but might be worth documenting so I put these changes in a separate commit #977 .
The two PRs interfere but rebasing should just be matter to put measureU2 inside a preexisting section introduced by PR #977 , sorry for the trouble.

[affeldt-aist]

I also have a need for bigsetU_compact and finite_card_sum in a wip PR on a related topic.