Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 08:10 6bd6afaf

View on Github →

feat(data/nat/interval): finite intervals of naturals (#9507) This proves that ℕ is a locally_finite_order.

Estimated changes

added theorem nat.Icc_eq_range'
added theorem nat.Icc_succ_left
added theorem nat.Ioc_eq_range'
added theorem nat.Ioo_eq_range'
added theorem nat.card_Icc
added theorem nat.card_Ioc
added theorem nat.card_Ioo
added theorem nat.card_fintype_Icc
added theorem nat.card_fintype_Ioc
added theorem nat.card_fintype_Ioo