Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 15:09 7a5d15a9

View on Github →

feat(data/pnat/interval): Finite intervals in ℕ+ (#9534) This proves that ℕ+ is a locally finite order.

Estimated changes

Created src/data/pnat/interval.lean

added theorem pnat.Icc_eq_finset_subtype

added theorem pnat.Ioc_eq_finset_subtype

added theorem pnat.Ioo_eq_finset_subtype

added theorem pnat.card_Icc

added theorem pnat.card_Ioc

added theorem pnat.card_Ioo

added theorem pnat.card_fintype_Icc

added theorem pnat.card_fintype_Ioc

added theorem pnat.card_fintype_Ioo

added theorem pnat.map_subtype_embedding_Icc

added theorem pnat.map_subtype_embedding_Ioc

added theorem pnat.map_subtype_embedding_Ioo