Commit 2022-12-22 13:12 418c4689

View on Github →

feat: port Order.Monotone.Odd (#1162)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Monotone/Odd.lean

added theorem antitone_of_odd_of_monotone_on_nonneg

added theorem monotone_of_odd_of_monotone_on_nonneg

added theorem strictAnti_of_odd_strictAnti_on_nonneg

added theorem strictMono_of_odd_strictMono_on_nonneg