Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 18:49 828e1004

View on Github →

feat(data/finset/interval): finset α is a locally finite order (#9963)

Estimated changes

added theorem finset.Iic_eq_powerset
added theorem finset.Iio_eq_ssubsets
added theorem finset.card_Icc_finset
added theorem finset.card_Ico_finset
added theorem finset.card_Ioc_finset
added theorem finset.card_Ioo_finset
added theorem finset.Icc_erase_left
added theorem finset.Icc_erase_right
modified theorem finset.Ico_insert_right
modified theorem finset.Ioo_insert_left
added theorem finset.left_mem_Icc
added theorem finset.left_mem_Ico
added theorem finset.right_mem_Icc
added theorem finset.right_mem_Ioc
modified theorem finset.right_not_mem_Ico
added theorem sdiff_le_sdiff_left
added theorem sdiff_le_sdiff_right
deleted theorem sdiff_le_sdiff_self
deleted theorem sdiff_le_self_sdiff
added theorem sdiff_lt_sdiff_right
added theorem sdiff_sup_cancel
added theorem sup_sdiff_cancel_right
deleted theorem sup_sdiff_of_le