Commit 2023-02-01 08:30 81c86f69

View on Github →

feat Port Data.Multiset.LocallyFinite (#1980)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/LocallyFinite.lean

added theorem Multiset.Icc_eq_zero_iff

added theorem Multiset.Icc_eq_zero_of_lt

added theorem Multiset.Icc_self

added theorem Multiset.Ico_add_Ico_eq_Ico

added theorem Multiset.Ico_cons_right

added theorem Multiset.Ico_disjoint_Ico

added theorem Multiset.Ico_eq_zero_iff

added theorem Multiset.Ico_eq_zero_of_le

added theorem Multiset.Ico_filter_le

added theorem Multiset.Ico_filter_le_left

added theorem Multiset.Ico_filter_le_of_le_left

added theorem Multiset.Ico_filter_le_of_left_le

added theorem Multiset.Ico_filter_le_of_right_le

added theorem Multiset.Ico_filter_lt

added theorem Multiset.Ico_filter_lt_of_le_left

added theorem Multiset.Ico_filter_lt_of_le_right

added theorem Multiset.Ico_filter_lt_of_right_le

added theorem Multiset.Ico_inter_Ico

added theorem Multiset.Ico_inter_Ico_of_le

added theorem Multiset.Ico_self

added theorem Multiset.Ico_sub_Ico_left

added theorem Multiset.Ico_sub_Ico_right

added theorem Multiset.Ico_subset_Ico_iff

added theorem Multiset.Ioc_eq_zero_iff

added theorem Multiset.Ioc_eq_zero_of_le

added theorem Multiset.Ioc_self

added theorem Multiset.Ioo_cons_left

added theorem Multiset.Ioo_eq_zero

added theorem Multiset.Ioo_eq_zero_iff

added theorem Multiset.Ioo_eq_zero_of_le

added theorem Multiset.Ioo_self

added theorem Multiset.card_Ico_eq_card_Icc_sub_one

added theorem Multiset.card_Ioc_eq_card_Icc_sub_one

added theorem Multiset.card_Ioo_eq_card_Icc_sub_two

added theorem Multiset.card_Ioo_eq_card_Ico_sub_one

added theorem Multiset.left_mem_Icc

added theorem Multiset.left_mem_Ico

added theorem Multiset.left_not_mem_Ioc

added theorem Multiset.left_not_mem_Ioo

added theorem Multiset.map_add_left_Icc

added theorem Multiset.map_add_left_Ico

added theorem Multiset.map_add_left_Ioc

added theorem Multiset.map_add_left_Ioo

added theorem Multiset.map_add_right_Icc

added theorem Multiset.map_add_right_Ico

added theorem Multiset.map_add_right_Ioc

added theorem Multiset.map_add_right_Ioo

added theorem Multiset.nodup_Icc

added theorem Multiset.nodup_Ico

added theorem Multiset.nodup_Ioc

added theorem Multiset.nodup_Ioo

added theorem Multiset.right_mem_Icc

added theorem Multiset.right_mem_Ioc

added theorem Multiset.right_not_mem_Ico

added theorem Multiset.right_not_mem_Ioo