Commit 2025-08-08 15:38 fe81dd44

View on Github →

feat(MeasureTheory): add def support of a measure, and related API (#27680) The definition of support given in terms of neighborhood filters, as well as basic topological lemmas including those related to restricted measures, proof that the support of the sum of measures is the union of the supports, and proof that support is monotone with respect to absolute continuity of measures.

Estimated changes