Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-19 23:18 9ac7c0c8

View on Github →

feat(data/finset/basic): insert and erase lemmas (#18729) Interaction of insert and erase with inter, union and disjoint.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.disjoint_erase_comm

added theorem finset.disjoint_of_erase_left

added theorem finset.disjoint_of_erase_right

added theorem finset.erase_eq

added theorem finset.erase_inter

added theorem finset.erase_inter_comm

added theorem finset.erase_sdiff_comm

added theorem finset.erase_sdiff_distrib

added theorem finset.erase_union_distrib

added theorem finset.erase_union_of_mem

added theorem finset.insert_inter_distrib

added theorem finset.insert_union_comm

added theorem finset.inter_erase

modified theorem finset.sdiff_erase

added theorem finset.sdiff_erase_self

added theorem finset.sdiff_sdiff_eq_sdiff_union

added theorem finset.sdiff_singleton_eq_self

deleted theorem finset.sdiff_singleton_not_mem_eq_self

added theorem finset.sdiff_union_erase_cancel

added theorem finset.sdiff_union_sdiff_cancel

added theorem finset.union_erase_of_mem

added theorem finset.union_sdiff_cancel_left

added theorem finset.union_sdiff_cancel_right

added theorem finset.union_subset_union_left

added theorem finset.union_subset_union_right

Modified src/data/set/basic.lean

added theorem set.diff_diff_eq_sdiff_union

added theorem set.diff_union_diff_cancel

Modified src/order/boolean_algebra.lean

added theorem codisjoint_himp_self_left

added theorem codisjoint_himp_self_right

added theorem disjoint_sdiff_comm

added theorem himp_le

Modified src/order/heyting/basic.lean

added theorem codisjoint.himp_le_of_right_le

added theorem disjoint.le_sdiff_of_le_left