Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 14:16 a07d1de4

View on Github →

feat(data/fin/interval): Finite intervals in fin n (#9523)

Estimated changes

Created src/data/fin/interval.lean

added theorem fin.Icc_eq_finset_subtype

added theorem fin.Ioc_eq_finset_subtype

added theorem fin.Ioo_eq_finset_subtype

added theorem fin.card_Icc

added theorem fin.card_Ioc

added theorem fin.card_Ioo

added theorem fin.card_fintype_Icc

added theorem fin.card_fintype_Ioc

added theorem fin.card_fintype_Ioo

added theorem fin.map_subtype_embedding_Icc

added theorem fin.map_subtype_embedding_Ioc

added theorem fin.map_subtype_embedding_Ioo