Commit 2023-04-03 12:12 5d6642d6

View on Github →

feat: port Data.Finset.Interval (#2169)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Basic.lean

Created Mathlib/Data/Finset/Interval.lean

added theorem Finset.Icc_eq_filter_powerset

added theorem Finset.Icc_eq_image_powerset

added theorem Finset.Ico_eq_filter_ssubsets

added theorem Finset.Ico_eq_image_ssubsets

added theorem Finset.Iic_eq_powerset

added theorem Finset.Iio_eq_ssubsets

added theorem Finset.Ioc_eq_filter_powerset

added theorem Finset.Ioo_eq_filter_ssubsets

added theorem Finset.card_Icc_finset

added theorem Finset.card_Ico_finset

added theorem Finset.card_Iic_finset

added theorem Finset.card_Iio_finset

added theorem Finset.card_Ioc_finset

added theorem Finset.card_Ioo_finset