Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 13:24 9be12dd5

View on Github →

feat(order/locally_finite): introduce locally finite orders (#9464) The new typeclass locally_finite_order homogeneizes treatment of intervals as finsets and multisets. finset.Ico is now available for all locally finite orders (instead of being ℕ-specialized), rendering finset.Ico_ℤ and pnat.Ico useless. This PR also introduces the long-awaited finset.Icc, finset.Ioc, finset.Ioo, and finset.Ici, finset.Ioi (for order_tops) and finset.Iic, finset.Iio (for order_bots), and the multiset variations thereof.

Estimated changes

added theorem and_and_and_comm
added def finset.Icc
added def finset.Ici
added theorem finset.Ici_eq_Icc
added def finset.Iic
added theorem finset.Iic_eq_Icc
added def finset.Ioc
added def finset.Ioi
added theorem finset.Ioi_eq_Ioc
added def finset.Ioo
added theorem finset.coe_Icc
added theorem finset.coe_Ici
added theorem finset.coe_Iic
added theorem finset.coe_Ioc
added theorem finset.coe_Ioi
added theorem finset.coe_Ioo
added theorem finset.mem_Icc
added theorem finset.mem_Ici
added theorem finset.mem_Iic
added theorem finset.mem_Ioc
added theorem finset.mem_Ioi
added theorem finset.mem_Ioo
added theorem finset.subtype_Icc_eq
added theorem finset.subtype_Ioc_eq
added theorem finset.subtype_Ioo_eq
added def multiset.Icc
added def multiset.Ici
added def multiset.Iic
added def multiset.Ioc
added def multiset.Ioi
added def multiset.Ioo
added theorem multiset.mem_Icc
added theorem multiset.mem_Ici
added theorem multiset.mem_Iic
added theorem multiset.mem_Ioc
added theorem multiset.mem_Ioi
added theorem multiset.mem_Ioo
added theorem set.finite_Icc
added theorem set.finite_Ici
added theorem set.finite_Iic
added theorem set.finite_Ioc
added theorem set.finite_Ioi
added theorem set.finite_Ioo