Theorem Filter.HasBasis.smallSets

Modification history

2023-12-04 18:10
Mathlib/Order/Filter/SmallSets.lean
feat(Order/Filter): add `Filter.tendsto_image_smallSets` (#8811) …
Deleted Filter.HasBasis.smallSetsView on Github →
2023-01-24 10:06
Mathlib/Order/Filter/SmallSets.lean
Feat: port Order.Filter.SmallSets (#1810)
Added Filter.HasBasis.smallSetsView on Github →