Def MeasureTheory.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.embeddingReal View on Github →

2024-04-16 12:43

Mathlib/MeasureTheory/Constructions/Polish.lean

feat(Probability/Kernel): disintegration of finite kernels (#10603) …

Added MeasureTheory.embeddingReal View on Github →