Commit 2025-04-06 07:37 e91df4f0

View on Github →

feat(MeasureTheory): the map of a tight measure set by a continuous function is tight (#23535)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Tight.lean

added theorem MeasureTheory.IsTightMeasureSet.map

modified theorem MeasureTheory.IsTightMeasureSet.of_compactSpace

modified def MeasureTheory.IsTightMeasureSet

modified theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegular

modified theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT