Commit 2023-05-21 16:29 96469563

View on Github →

feat: port MeasureTheory.Constructions.Polish (#4064)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/Polish.lean

added theorem Continuous.measurableEmbedding

added theorem ContinuousOn.measurableEmbedding

added theorem IsClosed.analyticSet

added theorem IsClosed.measurableSet_image_of_continuousOn_injOn

added theorem IsOpen.analyticSet_image

added theorem Measurable.exists_continuous

added theorem Measurable.measurableEmbedding

added theorem MeasurableSet.analyticSet

added theorem MeasurableSet.image_of_continuousOn_injOn

added theorem MeasurableSet.image_of_measurable_injOn

added theorem MeasurableSet.isClopenable

added theorem MeasureTheory.AnalyticSet.iInter

added theorem MeasureTheory.AnalyticSet.iUnion

added theorem MeasureTheory.AnalyticSet.image_of_continuous

added theorem MeasureTheory.AnalyticSet.image_of_continuousOn

added theorem MeasureTheory.AnalyticSet.measurablySeparable

added theorem MeasureTheory.MeasurablySeparable.iUnion

added def MeasureTheory.MeasurablySeparable

added theorem MeasureTheory.analyticSet_empty

added theorem MeasureTheory.analyticSet_iff_exists_polishSpace_range

added theorem MeasureTheory.analyticSet_range_of_polishSpace

added theorem MeasureTheory.exists_measurableEmbedding_real

added theorem MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite

added theorem MeasureTheory.exists_subset_real_measurableEquiv

added theorem MeasureTheory.isClopenable_iff_measurableSet

added theorem MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable

added theorem MeasureTheory.measurableSet_exists_tendsto

added theorem MeasureTheory.measurableSet_range_of_continuous_injective

added theorem MeasureTheory.measurablySeparable_range_of_disjoint