Commit 2025-12-14 14:45 bf4d61f4

View on Github →

chore: IsTightMeasureSet_iff_exists_isCompact_measure_compl_le should be lower case (#32873)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Tight.lean

deleted theorem MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_le

added theorem MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le

Modified Mathlib/MeasureTheory/Measure/TightNormed.lean