Def MeasureTheory.IsTightMeasureSet

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 View on Github →

2025-02-25 15:05

Mathlib/MeasureTheory/Measure/Tight.lean

feat: define tight sets of measures (#21955) …

Added MeasureTheory.IsTightMeasureSet View on Github →