English
If s is star-convex at x and y ∈ s, with t in [0,1], then x + t·y ∈ s.
Русский
Если s звёздочно выпукло относительно x, и y ∈ s, и t ∈ [0,1], то x + t·y ∈ s.
LaTeX
$$$\\text{StarConvex}_{\\mathbb{K}}(x,s) \\wedge y\\in s \\Rightarrow \\forall t\\in\\mathbb{K}, 0\\le t \\le 1:\\ x + t\\cdot y \\in s$$$
Lean4
theorem add_smul_sub_mem (hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) :
x + t • (y - x) ∈ s := by
apply hs.segment_subset hy
rw [segment_eq_image']
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩