Theorem Filter.Eventually.exists_mem_basis_of_smallSets

Modification history

2025-01-28 07:32
Mathlib/Order/Filter/SmallSets.lean
feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
Added Filter.Eventually.exists_mem_basis_of_smallSetsView on Github →