Commit 2023-01-13 22:32 9f26ebf2

feat(analysis/convex/intrinsic): Intrinsic interior and frontier (#18027) Defines the intrinsic interior, closure and boundary of a set in a normed additive torsor (e.g., a real vector space or one of its nonempty affine subspaces). Results:

• Simple lemmas about those definitions
• affine_isometry.image_intrinsic_interior: The image of the intrinsic interior under an affine isometry is the relative interior of the image.
• set.nonempty.intrinsic_interior: The intrinsic interior of a nonempty convex set is nonempty.