Commit 2025-04-17 13:24 9ebc6664

View on Github →

feat(Interval/Finset/Fin): add lemmas about Finset.image (#23420) ... and Finset.map. Also deprecate 2 lemmas that @[simp]lified in the other direction.

Estimated changes

modified theorem Finset.card_attachFin
modified theorem Finset.mem_attachFin
modified theorem Fin.Iio_castSucc
modified theorem Fin.Ioi_succ
added theorem Fin.map_addNatEmb_Icc
added theorem Fin.map_addNatEmb_Ici
added theorem Fin.map_addNatEmb_Ico
added theorem Fin.map_addNatEmb_Ioc
added theorem Fin.map_addNatEmb_Ioi
added theorem Fin.map_addNatEmb_Ioo
added theorem Fin.map_addNatEmb_uIcc
added theorem Fin.map_castAddEmb_Icc
added theorem Fin.map_castAddEmb_Ici
added theorem Fin.map_castAddEmb_Ico
added theorem Fin.map_castAddEmb_Iic
added theorem Fin.map_castAddEmb_Iio
added theorem Fin.map_castAddEmb_Ioc
added theorem Fin.map_castAddEmb_Ioi
added theorem Fin.map_castAddEmb_Ioo
added theorem Fin.map_castLEEmb_Icc
added theorem Fin.map_castLEEmb_Ico
added theorem Fin.map_castLEEmb_Iic
added theorem Fin.map_castLEEmb_Iio
added theorem Fin.map_castLEEmb_Ioc
added theorem Fin.map_castLEEmb_Ioo
added theorem Fin.map_castLEEmb_uIcc
added theorem Fin.map_finCongr_Icc
added theorem Fin.map_finCongr_Ici
added theorem Fin.map_finCongr_Ico
added theorem Fin.map_finCongr_Iic
added theorem Fin.map_finCongr_Iio
added theorem Fin.map_finCongr_Ioc
added theorem Fin.map_finCongr_Ioi
added theorem Fin.map_finCongr_Ioo
added theorem Fin.map_finCongr_uIcc
added theorem Fin.map_natAddEmb_Icc
added theorem Fin.map_natAddEmb_Ici
added theorem Fin.map_natAddEmb_Ico
added theorem Fin.map_natAddEmb_Ioc
added theorem Fin.map_natAddEmb_Ioi
added theorem Fin.map_natAddEmb_Ioo
added theorem Fin.map_natAddEmb_uIcc
added theorem Fin.map_revPerm_Icc
added theorem Fin.map_revPerm_Ici
added theorem Fin.map_revPerm_Ico
added theorem Fin.map_revPerm_Iic
added theorem Fin.map_revPerm_Iio
added theorem Fin.map_revPerm_Ioc
added theorem Fin.map_revPerm_Ioi
added theorem Fin.map_revPerm_Ioo
added theorem Fin.map_revPerm_uIcc
added theorem Fin.map_succEmb_Icc
added theorem Fin.map_succEmb_Ici
added theorem Fin.map_succEmb_Ico
added theorem Fin.map_succEmb_Iic
added theorem Fin.map_succEmb_Iio
added theorem Fin.map_succEmb_Ioc
added theorem Fin.map_succEmb_Ioi
added theorem Fin.map_succEmb_Ioo
added theorem Fin.map_succEmb_uIcc
modified theorem Fin.map_valEmbedding_Icc
modified theorem Fin.map_valEmbedding_Ici
modified theorem Fin.map_valEmbedding_Ico
modified theorem Fin.map_valEmbedding_Iic
modified theorem Fin.map_valEmbedding_Iio
modified theorem Fin.map_valEmbedding_Ioc
modified theorem Fin.map_valEmbedding_Ioi
modified theorem Fin.map_valEmbedding_Ioo
modified theorem Fin.map_valEmbedding_uIcc