Closed affeldt-aist closed 4 weeks ago
I also think that lebesgue_measure.v
should be split, it not well named anyway, its first part is about real-valued measurable functions, I didn't go as far as appending its first part to measure.v
because the latter is already very long, a new file like measurable_realfun.v
might be better, what about recording the splitting idea as a issue for later (unless you think it is a better idea to do it now)?
I think a measurable_realfun.v
would be great. But it doesn't have to happen now. An issue is sufficient.
Motivation for this change
fixes #1313
This PR also shuffles the contents of the file
lebesgue_measure.v
so that lemmas that do not depend on Lebesgue's measure appear before it (the Egorov theorem in particular).Checklist
- [ ] added corresponding entries inCHANGELOG_UNRELEASED.md
Reference: How to document
Reminder to reviewers