Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-10 14:47 0d9cb85e

View on Github →

chore(order/filter): a few more lemmas about eventually and set operations (#5686)

Estimated changes

Modified src/data/set/basic.lean

modified theorem set.inter_diff_self

modified theorem set.inter_union_compl

modified theorem set.inter_union_diff

modified theorem set.union_diff_left

modified theorem set.union_diff_right

Modified src/data/set/disjointed.lean

added theorem pairwise.mono

Modified src/order/filter/basic.lean

added theorem filter.eventually_le.compl

added theorem filter.eventually_le.diff

added theorem filter.eventually_le.inter

added theorem filter.eventually_le.union

Modified src/order/filter/countable_Inter.lean

added theorem eventually_eq.countable_Inter

added theorem eventually_eq.countable_Union

added theorem eventually_eq.countable_bInter

added theorem eventually_eq.countable_bUnion

added theorem eventually_le.countable_Inter

added theorem eventually_le.countable_Union

added theorem eventually_le.countable_bInter

added theorem eventually_le.countable_bUnion