Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 13:13 947c3c6d

View on Github →

refactor(order/locally_finite): Allow finset.Iix/finset.Ixi on empty types (#14430) Define locally_finite_order_top and locally_finite_order_bot are redefine Ici, Ioi, iic, Iio using them. Those new typeclasses are the same as locally_finite_order + order_top/order_bot, except that they allow the empty type, which is a surprisingly useful feature.

Estimated changes

modified theorem gram_schmidt_zero
modified theorem fin.Ici_eq_finset_subtype
modified theorem fin.Iic_eq_finset_subtype
modified theorem fin.Iio_eq_finset_subtype
modified theorem fin.Ioi_eq_finset_subtype
modified theorem fin.card_Ici
modified theorem fin.card_Ioi
modified theorem fin.card_filter_ge
modified theorem fin.card_filter_gt
modified theorem fin.card_filter_le
modified theorem fin.card_filter_lt_lt
modified theorem fin.card_fintype_Ici
modified theorem fin.card_fintype_Ioi
modified theorem finset.Icc_subset_Ici_self
modified theorem finset.Icc_subset_Iic_self
modified theorem finset.Ico_subset_Ici_self
modified theorem finset.Ico_subset_Iio_self
modified theorem finset.Iio_subset_Iic_self
modified theorem finset.Ioc_subset_Iic_self
modified theorem finset.Ioc_subset_Ioi_self
modified theorem finset.Ioi_subset_Ici_self
modified theorem finset.Ioo_subset_Ici_self
modified theorem finset.Ioo_subset_Iic_self
modified theorem finset.Ioo_subset_Iio_self
modified theorem finset.Ioo_subset_Ioi_self
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_lt_eq_Ioi
modified theorem nat.card_Iic
modified theorem nat.card_Iio
added theorem Icc_of_dual
added theorem Ici_of_dual
added theorem Ici_to_dual
added theorem Ico_of_dual
added theorem Iic_of_dual
added theorem Iic_to_dual
added theorem Iio_of_dual
added theorem Iio_to_dual
added theorem Ioc_of_dual
added theorem Ioi_of_dual
added theorem Ioi_to_dual
added theorem Ioo_of_dual
modified def finset.Ici
modified def finset.Iic
modified def finset.Iio
modified def finset.Ioi
modified theorem finset.coe_Ici
modified theorem finset.coe_Iic
modified theorem finset.coe_Iio
modified theorem finset.coe_Ioi
modified theorem finset.mem_Ici
modified theorem finset.mem_Iic
modified theorem finset.mem_Iio
modified theorem finset.mem_Ioi
added theorem finset.subtype_Ici_eq
added theorem finset.subtype_Iic_eq
added theorem finset.subtype_Iio_eq
added theorem finset.subtype_Ioi_eq