Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.lift'_inf_powerset

Modification history

2022-04-24 20:37
src/order/filter/lift.lean
refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)
Deleted filter.lift'_inf_powersetView on Github →
2020-08-14 12:28
src/order/filter/lift.lean
chore(*): assorted lemmas for FTC-1 (#3755) …
Added filter.lift'_inf_powersetView on Github →