Commit 2022-12-04 13:06 96bcd37a

View on Github →

feat: Match mathlib#17801 (#839)

feat: Match mathlib#17801
fix proof

Estimated changes

Modified Mathlib/Order/Monotone.lean

modified theorem antitoneOn_univ

modified theorem monotoneOn_univ

added theorem not_monotone_not_antitone_iff_exists_le_le

added theorem not_monotone_not_antitone_iff_exists_lt_lt

modified theorem strictAntiOn_univ

modified theorem strictMonoOn_univ