Commit 2025-12-14 14:45 a3ead088

View on Github →

feat: more API for FiniteMeasure and ProbabilityMeasure (#32784)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure

modified theorem MeasureTheory.FiniteMeasure.continuous_mass

added theorem MeasureTheory.FiniteMeasure.mass_comap_le

added theorem MeasureTheory.FiniteMeasure.mass_map_le

added theorem MeasureTheory.FiniteMeasure.measureReal_eq_coe_coeFn

added theorem MeasureTheory.FiniteMeasure.restrict_union

added theorem MeasureTheory.FiniteMeasure.restrict_univ

added theorem MeasureTheory.FiniteMeasure.toMeasure_comap

added theorem MeasureTheory.FiniteMeasure.toMeasure_mk

added theorem MeasureTheory.FiniteMeasure.toMeasure_sum

added theorem Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.range_toFiniteMeasure

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

added theorem MeasureTheory.isProbabilityMeasure_iff_real

modified theorem MeasureTheory.probReal_univ