mathlib3

9e8bac05 - feat(data/finset): monotone maps preserve the maximum of a finset