Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 15:13 c8d14294

View on Github →

feat(data/{finset,multiset}/locally_finite): Simple interval lemmas (#9877) (finset/multiset).image_add_(left/right)_Ixx and multiset.nodup_Ixx

Estimated changes

Modified src/algebra/big_operators/intervals.lean

modified theorem finset.prod_Ico_add

modified theorem finset.sum_Ico_add

Modified src/data/finset/locally_finite.lean

deleted theorem finset.image_add_const_Icc

deleted theorem finset.image_add_const_Ico

deleted theorem finset.image_add_const_Ioc

deleted theorem finset.image_add_const_Ioo

added theorem finset.image_add_left_Icc

added theorem finset.image_add_left_Ico

added theorem finset.image_add_left_Ioc

added theorem finset.image_add_left_Ioo

added theorem finset.image_add_right_Icc

added theorem finset.image_add_right_Ico

added theorem finset.image_add_right_Ioc

added theorem finset.image_add_right_Ioo

Modified src/data/multiset/locally_finite.lean

deleted theorem multiset.map_add_const_Icc

deleted theorem multiset.map_add_const_Ioc

deleted theorem multiset.map_add_const_Ioo

added theorem multiset.map_add_left_Icc

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_Ioc

added theorem multiset.map_add_right_Ioo

added theorem multiset.nodup_Icc

added theorem multiset.nodup_Ioc

added theorem multiset.nodup_Ioo