Commit 2025-04-07 15:42 e37082f6

View on Github →

refactor(Interval/Finset/Fin): use Finset.attachFin (#23738) This way we don't need to test i < n for each i in an interval during evaluation.

Estimated changes

modified theorem Fin.Icc_eq_finset_subtype
modified theorem Fin.Ici_eq_finset_subtype
modified theorem Fin.Ico_eq_finset_subtype
modified theorem Fin.Iic_eq_finset_subtype
modified theorem Fin.Iio_eq_finset_subtype
modified theorem Fin.Ioc_eq_finset_subtype
modified theorem Fin.Ioi_eq_finset_subtype
modified theorem Fin.Ioo_eq_finset_subtype
added theorem Fin.attachFin_Icc
added theorem Fin.attachFin_Ico
added theorem Fin.attachFin_Iic
added theorem Fin.attachFin_Iio
added theorem Fin.attachFin_Ioc
added theorem Fin.attachFin_Ioo
added theorem Fin.attachFin_uIcc
modified theorem Fin.map_valEmbedding_Icc
modified theorem Fin.map_valEmbedding_Ico
modified theorem Fin.map_valEmbedding_Ioc
modified theorem Fin.map_valEmbedding_Ioo
modified theorem Fin.uIcc_eq_finset_subtype