Commit 2024-04-18 08:21 dd2a5bc0

View on Github →

feat: translations of ample sets are ample (#12046) This was supposed to be included in #11344, as even the module docstring shows Inspired by the sphere-eversion project (but golfed and slightly extended). Also, use namespace AmpleSet in the file.

Estimated changes

Modified Mathlib/Analysis/Convex/AmpleSet.lean

modified theorem AmpleSet.image

modified theorem AmpleSet.image_iff

modified theorem AmpleSet.preimage

modified theorem AmpleSet.preimage_iff

modified theorem AmpleSet.union

added theorem AmpleSet.vadd

added theorem AmpleSet.vadd_iff