Theorem MeasureTheory.isTightMeasureSet_of_inner_tendsto

Modification history

2025-04-07 13:30
Mathlib/MeasureTheory/Measure/TightNormed.lean
feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces (#23534) …
Added MeasureTheory.isTightMeasureSet_of_inner_tendstoView on Github →