Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto_small_sets_iff

Modification history

2022-04-24 20:37
src/order/filter/small_sets.lean
refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)
Modified filter.tendsto_small_sets_iffView on Github →
2022-04-22 06:47
src/order/filter/small_sets.lean
feat(order/filter/small_sets): define the filter of small sets (#13467) …
Added filter.tendsto_small_sets_iffView on Github →