mathlib
970f0746 - feat(analysis/convex/star): Star-convex sets (#10524)

Commit
4 years ago
feat(analysis/convex/star): Star-convex sets (#10524) This defines `star_convex 𝕜 x s` to mean that a set is star-convex (aka star-shaped, radially convex, or a star domain) at `x`. This means that every segment from `x` to a point in `s` is a subset of `s`.
Author
Parents
Loading