Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 15:09 d8968ba7

View on Github →

feat(algebra/order/functions): recursors and images under monotone maps (#9505)

Estimated changes

added theorem antitone_on.map_max
added theorem antitone_on.map_min
added theorem max_rec'
added theorem max_rec
added theorem min_rec'
added theorem min_rec
added theorem monotone_on.map_max
added theorem monotone_on.map_min