Commit 2025-12-16 21:41 89d31277

View on Github →

feat: use IsCompletelyPseudometrizable class in measure regularity statements (#32590) The new statements are slightly stronger than the old ones because they don't require the uniform structure to be given.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

deleted theorem MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet

modified theorem MeasureTheory.exists_isCompact_closure_measure_compl_lt

modified theorem MeasureTheory.innerRegularWRT_isCompact

modified theorem MeasureTheory.innerRegularWRT_isCompact_closure

modified theorem MeasureTheory.innerRegularWRT_isCompact_isClosed

modified theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen

modified theorem MeasureTheory.innerRegularWRT_isCompact_isOpen

modified theorem MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite

Modified Mathlib/MeasureTheory/Measure/Tight.lean

modified theorem MeasureTheory.isTightMeasureSet_singleton