Theorem MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_le

Modification history

2025-12-14 14:45
Mathlib/MeasureTheory/Measure/Tight.lean
chore: `IsTightMeasureSet_iff_exists_isCompact_measure_compl_le` should be lower case (#32873)
Deleted MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_leView on Github →
2025-02-25 15:05
Mathlib/MeasureTheory/Measure/Tight.lean
feat: define tight sets of measures (#21955) …
Added MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_leView on Github →