Commit 2024-07-28 10:33 65b8389e

View on Github →

chore(MeasureTheory/Constructions/Polish): split off embedding into the reals (#15208) Credit Rémy for https://github.com/leanprover-community/mathlib3/pull/18881

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/MeasureTheory/Constructions/Polish.lean to Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

deleted def MeasureTheory.embeddingReal

deleted theorem MeasureTheory.exists_measurableEmbedding_real

deleted theorem MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite

deleted theorem MeasureTheory.exists_subset_real_measurableEquiv

deleted theorem MeasureTheory.measurableEmbedding_embeddingReal

deleted theorem MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable

Created Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean

added def MeasureTheory.embeddingReal

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.measurableEmbedding_embeddingReal

added theorem MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

Modified Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

Modified Mathlib/Probability/Martingale/Convergence.lean