mathlib

585c5add - feat(data/finset): monotone maps preserve the maximum of a finset (#9035)