Theorem MeasureTheory.measurableEmbedding_embeddingReal

Modification history

2024-07-28 10:33
Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
chore(MeasureTheory/Constructions/Polish): split off embedding into the reals (#15208) …
Modified MeasureTheory.measurableEmbedding_embeddingRealView on Github →
2024-04-16 12:43
Mathlib/MeasureTheory/Constructions/Polish.lean
feat(Probability/Kernel): disintegration of finite kernels (#10603) …
Added MeasureTheory.measurableEmbedding_embeddingRealView on Github →