Commit 2021-10-02 13:51 241aad7b

View on Github →

feat(data/finset/interval): API for finset.Ixx (#9495) This proves basic results about finset.Ixx & co. Lemma names (should) match their set counterparts.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.coe_eq_singleton

Created src/data/finset/interval.lean

added theorem finset.Icc_eq_empty_iff

added theorem finset.Icc_eq_empty_of_lt

added theorem finset.Icc_self

added theorem finset.Ioc_eq_empty_iff

added theorem finset.Ioc_eq_empty_of_le

added theorem finset.Ioc_self

added theorem finset.Ioo_eq_empty

added theorem finset.Ioo_eq_empty_iff

added theorem finset.Ioo_eq_empty_of_le

added theorem finset.Ioo_self

added theorem finset.image_add_const_Icc

added theorem finset.image_add_const_Ioc

added theorem finset.image_add_const_Ioo

added theorem finset.nonempty_Icc

added theorem finset.nonempty_Ioc

added theorem finset.nonempty_Ioo