Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-03 22:32 dad7ecf9

View on Github →

feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801) Fulfill a todo I left a year ago. The proof is a big case bash on the relative positions of the four variables. I minimised it as much as I could. The end result mentions convexity, but this is mostly order theory.

Estimated changes

Modified src/analysis/convex/quasiconvex.lean

added theorem quasilinear_on.monotone_on_or_antitone_on

added theorem quasilinear_on_iff_monotone_on_or_antitone_on

Modified src/data/set/basic.lean

added theorem set.antitone_on_iff_antitone

added theorem set.monotone_on_iff_monotone

added theorem set.not_monotone_on_not_antitone_on_iff_exists_le_le

added theorem set.not_monotone_on_not_antitone_on_iff_exists_lt_lt

added theorem set.strict_anti_on_iff_strict_anti

added theorem set.strict_mono_on_iff_strict_mono

Modified src/data/set/intervals/basic.lean

Modified src/data/set/intervals/unordered_interval.lean

added theorem set.monotone_on_or_antitone_on_iff_interval

added theorem set.monotone_or_antitone_iff_interval

Modified src/order/monotone.lean

modified theorem antitone_on_univ

modified theorem monotone_on_univ

added theorem not_monotone_not_antitone_iff_exists_le_le

added theorem not_monotone_not_antitone_iff_exists_lt_lt

modified theorem strict_anti_on_univ

modified theorem strict_mono_on_univ