Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-05 19:53 111d73bf

View on Github →

feat(data/int/interval): Finite intervals in ℤ (#9526) This proves that ℤ is a locally finite order.

Estimated changes

added theorem int.Icc_eq_finset_map
added theorem int.Ioc_eq_finset_map
added theorem int.Ioo_eq_finset_map
added theorem int.card_Icc
added theorem int.card_Icc_of_le
added theorem int.card_Ioc
added theorem int.card_Ioc_of_le
added theorem int.card_Ioo
added theorem int.card_Ioo_of_lt
added theorem int.card_fintype_Icc
added theorem int.card_fintype_Ioc
added theorem int.card_fintype_Ioo