Theorem Filter.HasAntitoneBasis.tendsto_smallSets

Modification history

2023-01-24 10:06
Mathlib/Order/Filter/SmallSets.lean
Feat: port Order.Filter.SmallSets (#1810)
Added Filter.HasAntitoneBasis.tendsto_smallSetsView on Github →