Commit 2025-04-06 17:06 df8a91e8

View on Github →

feat(Finset/Fin): expand attachFin API (#23703) Also move Finset.fin to the same file.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finset/Fin.lean

added theorem Finset.attachFin_eq_fin

added theorem Finset.attachFin_ssubset_attachFin

added theorem Finset.attachFin_ssubset_attachFin_iff

added theorem Finset.attachFin_subset_attachFin

added theorem Finset.attachFin_subset_attachFin_iff

added theorem Finset.coe_attachFin

added theorem Finset.coe_fin

added theorem Finset.fin_map

added theorem Finset.fin_mono

added theorem Finset.fin_subset_fin

added theorem Finset.image_val_attachFin

added theorem Finset.map_valEmbedding_attachFin

added theorem Finset.mem_fin

Modified Mathlib/Data/Finset/Image.lean

deleted theorem Finset.coe_fin

deleted theorem Finset.fin_map

deleted theorem Finset.fin_mono

deleted theorem Finset.fin_subset_fin

deleted theorem Finset.mem_fin

Modified Mathlib/Order/Interval/Finset/Fin.lean