Star-convex sets #
This files defines star-convex sets (aka star domains, star-shaped set, radially convex set).
A set is star-convex at
x if every segment from
x to a point in the set is contained in the set.
This is the prototypical example of a contractible set in homotopy theory (by scaling every point
x), but has wider uses.
Note that this has nothing to do with star rings,
Star and co.
Main declarations #
StarConvex 𝕜 x s:
sis star-convex at
Implementation notes #
Instead of saying that a set is star-convex, we say a set is star-convex at a point. This has the advantage of allowing us to talk about convexity as being "everywhere star-convexity" and of making the union of star-convex sets be star-convex.
Incidentally, this choice means we don't need to assume a set is nonempty for it to be star-convex. Concretely, the empty set is star-convex at every point.
Balanced sets are star-convex.
The closure of a star-convex set is star-convex.
Star-convex sets are contractible.
A nonempty open star-convex set in
ℝ^n is diffeomorphic to the entire space.
Alternative definition of star-convexity, in terms of pointwise set operations.
The preimage of a star-convex set under an affine map is star-convex.
The image of a star-convex set under an affine map is star-convex.
Alternative definition of star-convexity, using division.