Theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT

Modification history

2025-04-06 07:37
Mathlib/MeasureTheory/Measure/Tight.lean
feat(MeasureTheory): the map of a tight measure set by a continuous function is tight (#23535)
Modified MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRTView on Github →
2025-02-25 15:05
Mathlib/MeasureTheory/Measure/Tight.lean
feat: define tight sets of measures (#21955) …
Added MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRTView on Github →