English
If x ∈ s and star-convex, then openSegment from x to any y ∈ s is contained in s; conversely, containment for all such y characterizes star-convexity.
Русский
Если x ∈ s и s звездообразно, то открытый сегмент от x до любого y ∈ s содержится в s; наоборот, вложение открытых сегментов по всем y характеризует звездообразность.
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \iff \forall y\in s,\ openSegment_{\mathbb{K}}(x,y) \subseteq s.$$$$
Lean4
theorem starConvex_iff_openSegment_subset [ZeroLEOneClass 𝕜] (hx : x ∈ s) :
StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s :=
starConvex_iff_segment_subset.trans <| forall₂_congr fun _ hy => (openSegment_subset_iff_segment_subset hx hy).symm