English
If s is balanced, then it is star-convex with respect to the origin: for every y ∈ s and t ∈ [0,1], t y ∈ s.
Русский
Если s сбалансировано, то оно звездо-выпукло относительно нуля: для любого y ∈ s и t ∈ [0,1] верно t y ∈ s.
LaTeX
$$$$\\text{If } s \\text{ is balanced, then } \\operatorname{StarConvex}_{\\mathbb{R}}(0,S).$$$$
Lean4
theorem starConvex (hs : Balanced ℝ s) : StarConvex ℝ 0 s :=
starConvex_zero_iff.2 fun _ hx a ha₀ ha₁ => hs _ (by rwa [Real.norm_of_nonneg ha₀]) (smul_mem_smul_set hx)