Theorem MeasureTheory.IsTightMeasureSet.map

Modification history

2026-08-26 08:21
Mathlib/MeasureTheory/Measure/Tight.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified MeasureTheory.IsTightMeasureSet.mapView on Github →
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)
Added MeasureTheory.IsTightMeasureSet.mapView on Github →