Intrinsic frontier and interior #
This file defines the intrinsic frontier, interior and closure of a set in a normed additive torsor. These are also known as relative frontier, interior, closure.
The intrinsic frontier/interior/closure of a set
s is the frontier/interior/closure of
considered as a set in its affine span.
The intrinsic interior is in general greater than the topological interior, the intrinsic frontier in general less than the topological frontier, and the intrinsic closure in cases of interest the same as the topological closure.
intrinsic_interior: Intrinsic interior
intrinsic_frontier: Intrinsic frontier
intrinsic_closure: Intrinsic closure
The main results are:
affine_isometry.image_intrinsic_closure: Intrinsic interiors/frontiers/closures commute with taking the image under an affine isometry.
set.nonempty.intrinsic_interior: The intrinsic interior of a nonempty convex set is nonempty.
- Chapter 8 of Barry Simon, Convexity
- Chapter 1 of [Rolf Schneider, Convex Bodies: The Brunn-Minkowski theory][schneider2013].
is_closed s → is_extreme 𝕜 s (intrinsic_frontier 𝕜 s)
x ∈ s → y ∈ intrinsic_interior 𝕜 s → open_segment 𝕜 x y ⊆ intrinsic_interior 𝕜 s
The intrinsic interior of a set is its interior considered as a set in its affine span.
The intrinsic frontier of a set is its frontier considered as a set in its affine span.
The intrinsic closure of a set is its closure considered as a set in its affine span.
Alias of the reverse direction of
Alias of the forward direction of
Note that neither
intrinsic_frontier is monotone.
The intrinsic interior of a nonempty convex set is nonempty.