English
Star-convexity at the origin is equivalent to a segment-closure condition: s is star-convex at 0 iff for every x in s and every a with 0 ≤ a ≤ 1, a·x ∈ s.
Русский
Звёздочная выпуклость относительно начала координат эквивалентна условию на отрезок: s звёздочно выпукло в 0 тогда и только тогда, когда для каждого x ∈ s и каждого a с 0 ≤ a ≤ 1 выполняется a·x ∈ s.
LaTeX
$$$\\text{StarConvex}_{\\mathbb{K}}(0,s) \\iff \\forall x\\in s,\\ \\forall a\\in\\mathbb{K},\\ 0\\le a \\le 1 \\Rightarrow a\\cdot x \\in s$$$
Lean4
theorem starConvex_zero_iff : StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s :=
by
refine forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩
·
simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
h (sub_nonneg_of_le ha₁) ha₀
· rw [smul_zero, zero_add]
exact h hb (by rw [← hab]; exact le_add_of_nonneg_left ha)
