Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 07:32 a0504eb3

View on Github →

refactor(data/*/interval): generalize finset.Ico to locally finite orders (#7987) finset.Ico currently goes ℕ → ℕ → finset ℕ. This generalizes it to α → α → finset α where locally_finite_order α. This also ports all the existing finset.Ico lemmas to the new API, which involves renaming and moving them to data.finset.interval or data.nat.interval depending on whether I could generalize them away from ℕ or not.

Estimated changes

added theorem fin.card_Ico
added theorem fin.card_fintype_Ico
added theorem finset.Ico_filter_le
added theorem finset.Ico_filter_lt
added theorem finset.Ico_inter_Ico
added theorem finset.Ico_self
added theorem finset.Ico_union_Ico'
added theorem finset.Ico_union_Ico
added theorem finset.Ioo_insert_left
added theorem finset.nonempty_Ico
deleted theorem finset.Ico.card
deleted theorem finset.Ico.coe_eq_Ico
deleted theorem finset.Ico.diff_left
deleted theorem finset.Ico.diff_right
deleted theorem finset.Ico.eq_empty_iff
deleted theorem finset.Ico.eq_empty_of_le
deleted theorem finset.Ico.filter_Ico_bot
deleted theorem finset.Ico.filter_le
deleted theorem finset.Ico.filter_lt
deleted theorem finset.Ico.image_add
deleted theorem finset.Ico.image_sub
deleted theorem finset.Ico.inter
deleted theorem finset.Ico.mem
deleted theorem finset.Ico.not_mem_top
deleted theorem finset.Ico.pred_singleton
deleted theorem finset.Ico.self_eq_empty
deleted theorem finset.Ico.subset_iff
deleted theorem finset.Ico.succ_singleton
deleted theorem finset.Ico.succ_top'
deleted theorem finset.Ico.succ_top
deleted theorem finset.Ico.to_finset
deleted theorem finset.Ico.union'
deleted theorem finset.Ico.union
deleted theorem finset.Ico.val
deleted theorem finset.Ico.zero_bot
deleted def finset.Ico
deleted theorem finset.Ico_ℤ.card
deleted theorem finset.Ico_ℤ.mem
deleted def finset.Ico_ℤ
deleted theorem finset.range_eq_Ico
deleted theorem set.Icc_ℕ_card
deleted theorem set.Icc_ℕ_finite
deleted theorem set.Icc_ℤ_card
deleted theorem set.Icc_ℤ_finite
deleted theorem set.Ico_pnat_card
deleted theorem set.Ico_ℕ_card
deleted theorem set.Ico_ℕ_finite
deleted theorem set.Ico_ℤ_card
deleted theorem set.Ico_ℤ_finite
deleted theorem set.Ioc_ℕ_card
deleted theorem set.Ioc_ℕ_finite
deleted theorem set.Ioc_ℤ_card
deleted theorem set.Ioc_ℤ_finite
deleted theorem set.Ioo_ℕ_card
deleted theorem set.Ioo_ℕ_finite
deleted theorem set.Ioo_ℤ_card
deleted theorem set.Ioo_ℤ_finite
added theorem int.Ico_eq_finset_map
added theorem int.card_Ico
added theorem int.card_Ico_of_le
added theorem int.card_fintype_Ico
added theorem finset.range_eq_Ico
added theorem nat.Icc_pred_right
added theorem nat.Ico_eq_range'
added theorem nat.Ico_pred_singleton
added theorem nat.Ico_succ_left
added theorem nat.Ico_succ_right
added theorem nat.Ico_succ_singleton
added theorem nat.Ico_succ_succ
added theorem nat.Ico_zero_eq_range
added theorem nat.Iio_eq_range
added theorem nat.card_Ico
added theorem nat.card_fintype_Ico
added theorem pnat.card_Ico
added theorem pnat.card_fintype_Ico
deleted theorem pnat.Ico.card
deleted theorem pnat.Ico.mem
deleted def pnat.Ico
added def finset.Ico
added theorem finset.Ico_subset_Ico
added def finset.Iio
added theorem finset.Iio_eq_Ico
added theorem finset.coe_Ico
added theorem finset.coe_Iio
added theorem finset.mem_Ico
added theorem finset.mem_Iio
added theorem finset.subtype_Ico_eq
added def multiset.Iio
added theorem multiset.mem_Iio
added theorem set.finite_Ico
added theorem set.finite_Iio