Def MeasureTheory.Measure.everywherePosSubset

Modification history

2024-05-14 17:58
Mathlib/MeasureTheory/Measure/EverywherePos.lean
chore: deprecate `@[pp_dot]` (#12609) …
Modified MeasureTheory.Measure.everywherePosSubsetView on Github →
2024-02-10 06:34
Mathlib/MeasureTheory/Measure/EverywherePos.lean
feat: everywhere positive sets for a measure (#10139) …
Added MeasureTheory.Measure.everywherePosSubsetView on Github →