feat(data/finset): monotone bijection from fin k (#2163)
* feat(data/finset): increasing bijection between fin k and an ordered finset
* fix build
* fix linter
* make argument explicit
* add equiv for fintype
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
