Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto.small_sets_mono

Modification history

2022-04-24 20:37

src/order/filter/small_sets.lean

refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)

Added filter.tendsto.small_sets_mono View on Github →