mathlib

9f26ebf2 - feat(analysis/convex/intrinsic): Intrinsic interior and frontier (#18027)

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. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>