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)
Added MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_leView on Github →