Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monotone_on.map_max

Modification history

2021-10-04 15:09
src/algebra/order/functions.lean
feat(algebra/order/functions): recursors and images under monotone maps (#9505)
Added monotone_on.map_maxView on Github →