Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-08-02 13:20 3ba15165

View on Github →

feat(analysis/convex/proj_Icc): Extending convex functions (#18797) Constantly extending monotone/antitone functions preserves their convexity.

Estimated changes

Modified src/algebra/order/module.lean

added theorem smul_max_of_nonpos

added theorem smul_min_of_nonpos

Modified src/algebra/order/monoid/lemmas.lean

added theorem max_mul_mul_le_max_mul_max'

added theorem min_mul_min_le_min_mul_mul'

Modified src/algebra/order/smul.lean

added theorem smul_max

added theorem smul_min

Created src/analysis/convex/proj_Icc.lean

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

added theorem antitone.image_Icc_subset

added theorem antitone_on.image_Icc_subset

added theorem monotone.image_Icc_subset

added theorem monotone_on.image_Icc_subset

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

added theorem antitone.image_uIcc_subset

added theorem antitone_on.image_uIcc_subset

added theorem monotone.image_uIcc_subset

added theorem monotone_on.image_uIcc_subset

Modified src/order/lattice.lean

added theorem antitone_on.map_inf

added theorem antitone_on.map_sup

added theorem antitone_on.of_map_inf

added theorem antitone_on.of_map_sup

added theorem monotone_on.map_inf

added theorem monotone_on.map_sup

added theorem monotone_on.of_map_inf

added theorem monotone_on.of_map_sup