Commit 2024-12-20 12:30 02bf40fb

View on Github →

feat: monovarying functions are simultaneously monotone (#20047) From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Monotone/MonovaryOrder.lean

added def MonovaryOrder

added theorem antivaryOn_iff_exists_antitoneOn_monotoneOn

added theorem antivaryOn_iff_exists_monotoneOn_antitoneOn

added theorem antivary_iff_exists_antitone_monotone

added theorem antivary_iff_exists_monotone_antitone

added theorem monovaryOn_iff_exists_antitoneOn

added theorem monovaryOn_iff_exists_monotoneOn

added theorem monovary_iff_exists_antitone

added theorem monovary_iff_exists_monotone