Commit 2023-10-06 14:17 caeb3fea

View on Github →

feat: Extending convex functions (#6339) Forward-ports https://github.com/leanprover-community/mathlib/pull/18797 The changes to Mathlib.Data.Set.Intervals.Basic were independently added to mathlib4 in Mathlib.Data.Set.Intervals.Image, so the #aligns have been added there instead of the original file.

Estimated changes

Modified Mathlib/Algebra/Order/Module.lean

added theorem smul_max_of_nonpos

added theorem smul_min_of_nonpos

Modified Mathlib/Algebra/Order/Monoid/Lemmas.lean

added theorem max_mul_mul_le_max_mul_max'

added theorem min_mul_min_le_min_mul_mul'

Modified Mathlib/Algebra/Order/SMul.lean

added theorem smul_max

added theorem smul_min

Modified Mathlib/Data/Set/Intervals/Basic.lean

Modified Mathlib/Data/Set/Intervals/Image.lean

Modified Mathlib/Order/Lattice.lean

added theorem AntitoneOn.of_map_inf

added theorem AntitoneOn.of_map_sup

added theorem MonotoneOn.of_map_inf

added theorem MonotoneOn.of_map_sup