Mathlib Changelog
v4
Changelog
About
Github
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