Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.monotone_small_sets

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.monotone_small_sets View on Github →