mathlib

2c5f36c4 - feat(data/finset/sort): an order embedding from fin (#11800)

feat(data/finset/sort): an order embedding from fin (#11800) Given a set `s` of at least `k` element in a linear order, there is an order embedding from `fin k` whose image is contained in `s`.