Commit 2023-11-13 16:29 5c9c13df

chore: split MeasureSpace.lean into 3 files (#8389) The original file MeasureSpace.lean is a mess of 4580 lines, with a lot of changes of namespaces, active variables, and so on. We split it into three files:

• MeasureSpace, with 2095 lines left (some stuff could still be moved to other files, but it already makes much more sense)
• Restrict, with everything on restriction of measures (1100 lines)
• Typeclasses, defining finite measures, sigma-finite measures, and so on (1443 lines) The new files are still large, but less so. This is 99% moving around and ensuring that variables and namespaces remain the same (#align statements have been very useful for this), and 1% adding classical in proofs and [Decidable ...] assumptions in statements, as I haven't opened Classical in the new files.