Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 02:35 a9481d97

View on Github →

feat(analysis/convex/basic): add lemmas about transformations of convex sets and functions (#3524)

Estimated changes

Modified src/analysis/convex/basic.lean

added theorem convex.affine_image

added theorem convex.affine_preimage

added theorem convex.combo_affine_apply

added theorem convex.combo_to_vadd

added theorem convex.translate_preimage_left

added theorem convex.translate_preimage_right

added theorem convex_on.comp_affine_map

added theorem convex_on.comp_linear_map

added theorem convex_on.translate_left

added theorem convex_on.translate_right

Modified src/analysis/convex/cone.lean