English
A set s is star-convex with respect to x if and only if for every y ∈ s the segment from x to y is contained in s.
Русский
Множество s звездообразно относительно точки x тогда и только тогда, когда для каждого y ∈ s отрезок от x до y содержится в s.
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \iff \forall y \in s,\ [x -[\mathbb{K}] y] \subseteq s.$$$$
Lean4
theorem starConvex_iff_segment_subset : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
by
constructor
· rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩
exact h hy ha hb hab
· rintro h y hy a b ha hb hab
exact h hy ⟨a, b, ha, hb, hab, rfl⟩