Commit 2024-04-17 16:06 726f2a5f

View on Github →

feat(MeasureTheory/Constructions/Polish): generalize topological assumptions to measurable ones. (#12069) Several theorems in MeasureTheory/Constructions/Polish.lean about measurable sets, functions, etc. assume that a space is a BorelSpace or OpensMeasurableSpace for some nice topology. This PR removes the topological data from such theorems when possible, replacing them with sufficient and natural assumptions on MeasurableSpace's. The old versions of the theorems still work automatically thanks to TC inference. TODO: Add CountablySeparated typeclass abbreviating HasCountableSeparatingOn _ MeasurableSet univ.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints

added theorem exists_opensMeasurableSpace_of_hasCountableSeparatingOn

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

modified theorem Measurable.map_measurableSpace_eq

modified theorem Measurable.measurableEmbedding

modified theorem Measurable.measurableSet_preimage_iff_inter_range

modified theorem Measurable.measurableSet_preimage_iff_of_surjective

modified theorem Measurable.measurableSet_preimage_iff_preimage_val

modified theorem Measurable.measurable_comp_iff_of_surjective

modified theorem Measurable.measurable_comp_iff_restrict

modified theorem MeasurableSet.image_of_measurable_injOn

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

added theorem MeasurableSpace.separatesPoints_iff