Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.isTightMeasureSet_singleton
Modification history
2025-04-07 13:30
Mathlib/MeasureTheory/Measure/Tight.lean
feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces (#23534) …
Added
MeasureTheory.isTightMeasureSet_singleton
View on Github →