Theorem MeasureTheory.Measure.support_mem_ae_of_isLindelof

Modification history

2025-08-08 15:38
Mathlib/MeasureTheory/Measure/Support.lean
feat(MeasureTheory): add def `support` of a measure, and related API (#27680) …
Added MeasureTheory.Measure.support_mem_ae_of_isLindelofView on Github →