Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 13:31 b9db1696

View on Github →

chore(order/locally_finite): fill in finset interval API (#11338) A bunch of statements about finset intervals, mimicking the set interval API and mostly proved using it. simp attributes are chosen as they were for sets. Also some golf.

Estimated changes

added theorem finset.Icc_diff_both
added theorem finset.Icc_eq_cons_Ico
added theorem finset.Icc_eq_cons_Ioc
modified theorem finset.Icc_erase_left
modified theorem finset.Icc_erase_right
added theorem finset.Icc_subset_Icc
added theorem finset.Ici_eq_cons_Ioi
added theorem finset.Ici_erase
added theorem finset.Ico_erase_left
modified theorem finset.Ico_insert_right
modified theorem finset.Ico_self
added theorem finset.Ico_subset_Ico
added theorem finset.Iic_eq_cons_Iio
added theorem finset.Iic_erase
added theorem finset.Iio_insert
added theorem finset.Ioc_erase_right
added theorem finset.Ioc_insert_left
modified theorem finset.Ioc_self
added theorem finset.Ioc_subset_Ioc
added theorem finset.Ioi_insert
modified theorem finset.Ioo_insert_left
modified theorem finset.Ioo_self
added theorem finset.Ioo_subset_Ioo
modified theorem finset.filter_ge_eq_Iic
modified theorem finset.filter_gt_eq_Iio
modified theorem finset.filter_le_eq_Ici
modified theorem finset.filter_le_le_eq_Icc
modified theorem finset.filter_le_lt_eq_Ico
modified theorem finset.filter_lt_eq_Ioi
modified theorem finset.filter_lt_le_eq_Ioc
modified theorem finset.filter_lt_lt_eq_Ioo
modified theorem finset.image_add_right_Icc
modified theorem finset.image_add_right_Ico
modified theorem finset.image_add_right_Ioc
modified theorem finset.image_add_right_Ioo
modified theorem finset.left_mem_Icc
modified theorem finset.left_mem_Ico
modified theorem finset.right_mem_Icc
modified theorem finset.right_mem_Ioc
deleted theorem finset.Ico_subset_Ico
modified theorem finset.coe_Icc
modified theorem finset.coe_Ico
modified theorem finset.coe_Ioc
modified theorem finset.coe_Ioo
modified theorem finset.mem_Icc
modified theorem finset.mem_Ici
modified theorem finset.mem_Ico
modified theorem finset.mem_Iic
modified theorem finset.mem_Iio
modified theorem finset.mem_Ioc
modified theorem finset.mem_Ioi
modified theorem finset.mem_Ioo