Commit 2023-04-24 08:51 04370794

View on Github →

feat: insert and erase lemmas (#3569) Match https://github.com/leanprover-community/mathlib/pull/18729

Estimated changes

Modified Mathlib/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 Mathlib/Data/Set/Basic.lean

added theorem Set.diff_diff_eq_sdiff_union

added theorem Set.diff_union_diff_cancel

Modified Mathlib/Order/BooleanAlgebra.lean

added theorem codisjoint_himp_self_left

added theorem codisjoint_himp_self_right

added theorem disjoint_sdiff_comm

added theorem himp_le

Modified Mathlib/Order/Heyting/Basic.lean

added theorem Codisjoint.himp_le_of_right_le

added theorem Disjoint.le_sdiff_of_le_left