Commit 2023-02-08 08:15 f92e0e35

View on Github →

feat: port Data.Finsupp.Interval (#2151)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Interval.lean

added theorem Finsupp.card_Icc

added theorem Finsupp.card_Ico

added theorem Finsupp.card_Iic

added theorem Finsupp.card_Iio

added theorem Finsupp.card_Ioc

added theorem Finsupp.card_Ioo

added theorem Finsupp.coe_rangeIcc

added theorem Finsupp.icc_eq

added theorem Finsupp.mem_rangeIcc_apply_iff

added theorem Finsupp.mem_rangeSingleton_apply_iff

added def Finsupp.rangeIcc

added theorem Finsupp.rangeIcc_support

added def Finsupp.rangeSingleton