Commit 2023-02-08 12:41 c16c0c41

View on Github →

feat: port Data.Dfinsupp.Interval (#2162)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dfinsupp/Interval.lean

added theorem Dfinsupp.Icc_eq

added theorem Dfinsupp.card_Icc

added theorem Dfinsupp.card_Ico

added theorem Dfinsupp.card_Iic

added theorem Dfinsupp.card_Iio

added theorem Dfinsupp.card_Ioc

added theorem Dfinsupp.card_Ioo

added theorem Dfinsupp.card_pi

added theorem Dfinsupp.mem_pi

added theorem Dfinsupp.mem_rangeIcc_apply_iff

added theorem Dfinsupp.mem_singleton_apply_iff

added def Dfinsupp.pi

added def Dfinsupp.rangeIcc

added theorem Dfinsupp.rangeIcc_apply

added def Dfinsupp.singleton

added theorem Dfinsupp.support_rangeIcc_subset

added theorem Finset.card_dfinsupp

added def Finset.dfinsupp

added theorem Finset.mem_dfinsupp_iff

added theorem Finset.mem_dfinsupp_iff_of_support_subset