Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-02 11:46 65598321

View on Github →

feat(order/filter/lift): a few lemmas about filter.lift' _ powerset (#3652)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.powerset_mono

added theorem set.powerset_nonempty

Modified src/order/filter/lift.lean

added theorem filter.eventually_lift'_iff

added theorem filter.eventually_lift'_powerset'

added theorem filter.eventually_lift'_powerset

added theorem filter.eventually_lift'_powerset_eventually

added theorem filter.eventually_lift'_powerset_forall