Commit 2024-04-10 10:42 147c3d0e

View on Github →

feat: ample sets in real vector spaces (#11344) From the sphere eversion project.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/AmpleSet.lean

added theorem AmpleSet.image

added theorem AmpleSet.image_iff

added theorem AmpleSet.preimage

added theorem AmpleSet.preimage_iff

added theorem AmpleSet.union

added def AmpleSet

added theorem ampleSet_empty

added theorem ampleSet_univ

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

modified theorem ContinuousAffineEquiv.eq_symm_apply

added theorem ContinuousAffineEquiv.image_preimage

added theorem ContinuousAffineEquiv.image_symm_image

added theorem ContinuousAffineEquiv.preimage_image

modified theorem ContinuousAffineEquiv.symm_apply_eq

added theorem ContinuousAffineEquiv.symm_image_image

modified theorem ContinuousAffineEquiv.symm_symm_apply