Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 07:33 41dd4da3

View on Github →

feat(data/multiset/interval): Intervals as multisets (#9588) This provides API for multiset.Ixx (except multiset.Ico).

Estimated changes

Modified src/data/multiset/erase_dup.lean

Created src/data/multiset/interval.lean

added theorem multiset.Icc_eq_zero_iff

added theorem multiset.Icc_eq_zero_of_lt

added theorem multiset.Icc_self

added theorem multiset.Ioc_eq_zero_iff

added theorem multiset.Ioc_eq_zero_of_le

added theorem multiset.Ioc_self

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.map_add_const_Icc

added theorem multiset.map_add_const_Ioc

added theorem multiset.map_add_const_Ioo