Def MeasureTheory.ProbabilityMeasure.toFiniteMeasure

Modification history

2024-08-16 08:13

Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

chore: a clean-up of files on finite measures, probability measures, and portmanteau theorem (#12822)

Modified MeasureTheory.ProbabilityMeasure.toFiniteMeasure View on Github →

2023-06-07 06:36

Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

feat: port MeasureTheory.Measure.ProbabilityMeasure (#4765)

Added MeasureTheory.ProbabilityMeasure.toFiniteMeasure View on Github →