Commit 2025-03-01 18:09 05cbcc8a

View on Github →

chore: add lemmas about List.finRange and Finset.sort (#22425) Also add Finset.val_univ_fin

Estimated changes

Modified Mathlib/Data/Finset/Sort.lean

added theorem Finset.image_orderEmbOfFin_univ

added theorem Finset.listMap_orderEmbOfFin_finRange

added theorem Finset.map_orderEmbOfFin_univ

added theorem Finset.sort_mk

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Finset.val_univ_fin

Modified Mathlib/Data/List/FinRange.lean

added theorem List.count_finRange

added theorem List.finRange_map_getElem