Commit 2023-01-26 12:46 3920c8ea

View on Github →

feat: port Data.Fin.Interval (#1846)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fin/Interval.lean

added theorem Fin.Icc_eq_finset_subtype

added theorem Fin.Ici_eq_finset_subtype

added theorem Fin.Ico_eq_finset_subtype

added theorem Fin.Iic_eq_finset_subtype

added theorem Fin.Iio_eq_finset_subtype

added theorem Fin.Ioc_eq_finset_subtype

added theorem Fin.Ioi_eq_finset_subtype

added theorem Fin.Ioo_eq_finset_subtype

added theorem Fin.card_Icc

added theorem Fin.card_Ici

added theorem Fin.card_Ico

added theorem Fin.card_Iic

added theorem Fin.card_Iio

added theorem Fin.card_Ioc

added theorem Fin.card_Ioi

added theorem Fin.card_Ioo

added theorem Fin.card_fintypeIcc

added theorem Fin.card_fintypeIci

added theorem Fin.card_fintypeIco

added theorem Fin.card_fintypeIic

added theorem Fin.card_fintypeIio

added theorem Fin.card_fintypeIoc

added theorem Fin.card_fintypeIoi

added theorem Fin.card_fintypeIoo

added theorem Fin.map_subtype_embedding_Icc

added theorem Fin.map_subtype_embedding_Ici

added theorem Fin.map_subtype_embedding_Ico

added theorem Fin.map_subtype_embedding_Iic

added theorem Fin.map_subtype_embedding_Iio

added theorem Fin.map_subtype_embedding_Ioc

added theorem Fin.map_subtype_embedding_Ioi

added theorem Fin.map_subtype_embedding_Ioo