Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 08:02 37c691f7

View on Github →

feat(analysis/convex/*): Convexity and subtraction (#14015) Now that we have a fair bit more pointwise operations on set, a few results can be (re)written using them. For example, existing lemmas about add and neg can be combined to give lemmas about sub.

Estimated changes

Modified src/analysis/convex/basic.lean

modified theorem convex.affine_image

deleted theorem convex.neg_preimage

modified theorem convex.sub

modified theorem convex.translate

added theorem convex.vadd

Modified src/analysis/convex/function.lean

added theorem concave_on.add_strict_concave_on

added theorem concave_on.sub

added theorem concave_on.sub_strict_convex_on

added theorem convex_on.add_strict_convex_on

added theorem convex_on.sub

added theorem convex_on.sub_strict_concave_on

added theorem strict_concave_on.add_concave_on

added theorem strict_concave_on.sub

added theorem strict_concave_on.sub_convex_on

added theorem strict_convex_on.add_convex_on

added theorem strict_convex_on.sub

added theorem strict_convex_on.sub_concave_on

Modified src/analysis/convex/star.lean

modified theorem star_convex.neg

deleted theorem star_convex.neg_preimage

added theorem star_convex.sub'

modified theorem star_convex.sub

Modified src/analysis/convex/strict.lean

modified theorem strict_convex.neg

deleted theorem strict_convex.neg_preimage

added theorem strict_convex.sub