Theorem Filter.HasBasis.eventually_smallSets

Modification history

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