Commit 2025-02-25 15:05 48ed0bdb

View on Github →

feat: define tight sets of measures (#21955) Co-authored by: Josha Dekker

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Tight.lean

added theorem MeasureTheory.IsTightMeasureSet.of_compactSpace

added def MeasureTheory.IsTightMeasureSet

added theorem MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_le

added theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegular

added theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT