Commit 2023-06-16 00:13 60c49568

View on Github →

chore: forward port leanprover-community/mathlib#19186 (#5080)

Estimated changes

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

added theorem borel_anti

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

added theorem Continuous.map_borel_eq

added theorem Continuous.map_eq_borel

added theorem Measurable.borelSpace_codomain

added theorem Measurable.map_measurableSpace_eq

added theorem Measurable.map_measurableSpace_eq_borel

added theorem Measurable.measurableSet_preimage_iff_inter_range

added theorem Measurable.measurableSet_preimage_iff_of_surjective

added theorem Measurable.measurableSet_preimage_iff_preimage_val

added theorem Measurable.measurable_comp_iff_of_surjective

added theorem Measurable.measurable_comp_iff_restrict

added theorem MeasurableSet.analyticSet_image

added theorem MeasureTheory.AnalyticSet.measurableSet_of_compl

modified theorem MeasureTheory.AnalyticSet.measurablySeparable

modified theorem MeasureTheory.measurablySeparable_range_of_disjoint