Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-10 12:55
1bc57918
View on Github →
feat: taking the product of probability measures is a continuous map (
#27932
)
Estimated changes
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
added
theorem
null_frontier_inter
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
added
theorem
MeasureTheory.FiniteMeasure.apply_union_le
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
modified
theorem
MeasureTheory.FiniteMeasure.prod_prod
added
theorem
MeasureTheory.ProbabilityMeasure.continuous_prod
modified
theorem
MeasureTheory.ProbabilityMeasure.prod_prod
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
added
theorem
MeasureTheory.ProbabilityMeasure.apply_union_le