Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-30 21:46 bf07fdbb

View on Github →

chore(data/finset/locally_finite): add more lemmas about one-sided intervals (#17033) This also:

  • adds new pi.locally_finite_order_bot and pi.locally_finite_order_top instances, and generalizes the lemmas needed to prove things about them.
  • generalizes some finsupp lemmas about intervals to arbitrary decidable arguments.

Estimated changes

added theorem dfinsupp.card_Iic
added theorem dfinsupp.card_Iio
added theorem finset.card_Iic_finset
added theorem finset.card_Iio_finset
modified theorem finset.Ici_eq_cons_Ioi
modified theorem finset.Ici_erase
modified theorem finset.Iic_eq_cons_Iio
modified theorem finset.Iic_erase
modified theorem finsupp.Icc_eq
modified theorem finsupp.card_Icc
modified theorem finsupp.card_Ico
added theorem finsupp.card_Iic
added theorem finsupp.card_Iio
modified theorem finsupp.card_Ioc
modified theorem finsupp.card_Ioo
modified def finsupp.range_Icc
added theorem pi.card_Ici
added theorem pi.card_Iic
added theorem pi.card_Iio
added theorem pi.card_Ioi
added theorem set.not_mem_Iio_self
added theorem set.not_mem_Ioi_self