Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-20 01:09 f467c816

View on Github →

feat(data/multiset): disjoint, nodup, finset ops

Estimated changes

Modified data/list/basic.lean

modified def list.disjoint

deleted theorem list.disjoint_append_of_disjoint_left

modified theorem list.erase_dup_append

modified theorem list.sublist_suffix_of_union

Modified data/multiset/basic.lean

modified def multiset.card

modified theorem multiset.card_cons

deleted theorem multiset.card_empty

modified theorem multiset.card_erase_of_mem

deleted theorem multiset.card_insert_le

deleted theorem multiset.card_insert_of_not_mem

modified theorem multiset.card_range

added theorem multiset.coe_disjoint

added theorem multiset.coe_erase_dup

added theorem multiset.coe_ndinsert

added theorem multiset.coe_ndinter

added theorem multiset.coe_ndunion

added theorem multiset.coe_nodup

added theorem multiset.coe_subset

added theorem multiset.cons_erase

added theorem multiset.cons_ndinter_of_mem

added theorem multiset.cons_ndunion

added theorem multiset.cons_subset

added theorem multiset.count_eq_one_of_mem

added theorem multiset.disjoint.symm

added def multiset.disjoint

added theorem multiset.disjoint_add_left

added theorem multiset.disjoint_add_right

added theorem multiset.disjoint_comm

added theorem multiset.disjoint_cons_left

added theorem multiset.disjoint_cons_right

added theorem multiset.disjoint_iff_ne

added theorem multiset.disjoint_left

added theorem multiset.disjoint_of_le_left

added theorem multiset.disjoint_of_le_right

added theorem multiset.disjoint_of_nodup_add

added theorem multiset.disjoint_of_subset_left

added theorem multiset.disjoint_of_subset_right

added theorem multiset.disjoint_right

added theorem multiset.disjoint_singleton

deleted theorem multiset.empty_inter

deleted theorem multiset.eq_cons_erase

deleted theorem multiset.eq_empty_of_card_eq_zero

deleted theorem multiset.eq_zero_of_le_zero

modified def multiset.erase

added def multiset.erase_dup

added theorem multiset.erase_dup_add

added theorem multiset.erase_dup_cons_of_mem

added theorem multiset.erase_dup_cons_of_not_mem

added theorem multiset.erase_dup_eq_self

added theorem multiset.erase_dup_le

deleted theorem multiset.erase_dup_map_erase_dup_eq

added theorem multiset.erase_dup_subset

added theorem multiset.erase_dup_zero

deleted theorem multiset.erase_empty

deleted theorem multiset.erase_eq_of_not_mem

deleted theorem multiset.erase_insert

deleted theorem multiset.erase_insert_subset

modified theorem multiset.erase_subset

deleted theorem multiset.erase_subset_erase

deleted theorem multiset.erase_subset_of_subset_insert

deleted theorem multiset.exists_mem_empty_iff

deleted theorem multiset.exists_mem_insert

deleted theorem multiset.exists_nat_subset_range

deleted theorem multiset.filter_false

deleted theorem multiset.filter_filter

deleted theorem multiset.filter_inter_filter_neg_eq

modified theorem multiset.filter_subset

modified theorem multiset.filter_union

deleted theorem multiset.filter_union_filter_neg_eq

deleted theorem multiset.forall_mem_empty_iff

deleted theorem multiset.forall_mem_insert

added theorem multiset.forall_mem_ne

deleted theorem multiset.image_empty

deleted theorem multiset.image_eq_empty_iff

deleted theorem multiset.image_filter

deleted theorem multiset.image_id

deleted theorem multiset.image_image

deleted theorem multiset.image_insert

deleted theorem multiset.image_inter

deleted theorem multiset.image_singleton

deleted theorem multiset.image_subset_image

deleted theorem multiset.image_to_multiset

deleted theorem multiset.image_to_multiset_of_nodup

deleted theorem multiset.image_union

deleted theorem multiset.insert_erase

deleted theorem multiset.insert_erase_subset

deleted theorem multiset.insert_inter_of_mem

deleted theorem multiset.insert_inter_of_not_mem

deleted theorem multiset.inter_assoc

modified theorem multiset.inter_comm

deleted theorem multiset.inter_distrib_left

deleted theorem multiset.inter_distrib_right

deleted theorem multiset.inter_empty

added theorem multiset.inter_eq_zero_iff_disjoint

deleted theorem multiset.inter_insert_of_mem

deleted theorem multiset.inter_insert_of_not_mem

added theorem multiset.inter_le_ndinter

deleted theorem multiset.inter_left_comm

deleted theorem multiset.inter_right_comm

deleted theorem multiset.inter_self

deleted theorem multiset.inter_singleton_of_mem

deleted theorem multiset.inter_singleton_of_not_mem

deleted theorem multiset.inter_subset_left

deleted theorem multiset.inter_subset_right

added theorem multiset.le_erase_dup

added theorem multiset.le_iff_subset

added theorem multiset.le_inter_iff

added theorem multiset.le_ndinsert_self

added theorem multiset.le_ndinter

added theorem multiset.le_ndunion_left

added theorem multiset.le_ndunion_right

added theorem multiset.le_zero

added theorem multiset.length_ndinsert_of_mem

added theorem multiset.length_ndinsert_of_not_mem

added theorem multiset.mem_add

deleted theorem multiset.mem_erase

added theorem multiset.mem_erase_dup

added theorem multiset.mem_erase_iff_of_nodup

deleted theorem multiset.mem_erase_of_ne_of_mem

added theorem multiset.mem_erase_of_nodup

modified theorem multiset.mem_filter

deleted theorem multiset.mem_image_iff

modified theorem multiset.mem_inter

deleted theorem multiset.mem_inter_of_mem

added theorem multiset.mem_ndinsert

added theorem multiset.mem_ndinsert_of_mem

added theorem multiset.mem_ndinsert_self

added theorem multiset.mem_ndinter

added theorem multiset.mem_ndunion

modified theorem multiset.mem_of_le

modified theorem multiset.mem_of_mem_erase

deleted theorem multiset.mem_of_mem_inter_left

deleted theorem multiset.mem_of_mem_inter_right

modified theorem multiset.mem_of_subset

modified theorem multiset.mem_range

deleted theorem multiset.mem_sdiff_iff

added theorem multiset.mem_union

added theorem multiset.ndinsert_le

added theorem multiset.ndinsert_of_mem

added theorem multiset.ndinsert_of_not_mem

added theorem multiset.ndinsert_zero

added def multiset.ndinter

added theorem multiset.ndinter_cons_of_not_mem

added theorem multiset.ndinter_eq_inter

added theorem multiset.ndinter_eq_zero_iff_disjoint

added theorem multiset.ndinter_le_left

added theorem multiset.ndinter_le_right

added theorem multiset.ndinter_subset_right

added def multiset.ndunion

added theorem multiset.ndunion_eq_union

added theorem multiset.ndunion_le

added theorem multiset.ndunion_le_add

added theorem multiset.ndunion_le_union

deleted theorem multiset.ne_empty_of_card_eq_succ

deleted theorem multiset.ne_of_mem_erase

added theorem multiset.nodup_add

added theorem multiset.nodup_add_of_nodup

added theorem multiset.nodup_cons

added theorem multiset.nodup_cons_of_nodup

added theorem multiset.nodup_erase_dup

added theorem multiset.nodup_erase_eq_filter

added theorem multiset.nodup_erase_of_nodup

added theorem multiset.nodup_ext

added theorem multiset.nodup_filter

added theorem multiset.nodup_iff_count_le_one

added theorem multiset.nodup_iff_le

added theorem multiset.nodup_inter_of_nodup

added theorem multiset.nodup_map

added theorem multiset.nodup_map_on

added theorem multiset.nodup_ndinsert

added theorem multiset.nodup_ndinter

added theorem multiset.nodup_ndunion

added theorem multiset.nodup_of_le

added theorem multiset.nodup_of_nodup_cons

added theorem multiset.nodup_of_nodup_map

added theorem multiset.nodup_product

added theorem multiset.nodup_range

added theorem multiset.nodup_singleton

added theorem multiset.nodup_zero

deleted theorem multiset.not_mem_erase

added theorem multiset.not_mem_of_nodup_cons

modified theorem multiset.not_mem_range_self

added theorem multiset.not_nodup_pair

modified def multiset.range

added theorem multiset.range_le

modified theorem multiset.range_subset

deleted theorem multiset.range_succ

deleted theorem multiset.range_zero

deleted theorem multiset.sdiff_inter_self

deleted theorem multiset.sdiff_subset_sdiff

deleted theorem multiset.sdiff_union_of_subset

added theorem multiset.singleton_disjoint

deleted theorem multiset.singleton_inter_of_mem

deleted theorem multiset.singleton_inter_of_not_mem

added theorem multiset.sub_le_self

modified theorem multiset.subset.refl

modified theorem multiset.subset.trans

added theorem multiset.subset_erase_dup

modified theorem multiset.subset_iff

deleted theorem multiset.subset_insert_iff

deleted theorem multiset.subset_insert_of_erase_subset

deleted theorem multiset.subset_inter

added theorem multiset.subset_ndunion_left

modified theorem multiset.subset_of_le

added theorem multiset.union_def

deleted theorem multiset.union_distrib_left

deleted theorem multiset.union_distrib_right

added theorem multiset.union_le_add

added theorem multiset.union_le_iff

added theorem multiset.zero_disjoint

added theorem multiset.zero_ndinter

added theorem multiset.zero_ndunion

modified theorem multiset.zero_subset