English
Star-convexity is preserved under linear maps: if s is star-convex at x, then f(x) is star-convex at f''s.
Русский
Звездообразность сохраняется под линейными отображениями: если s звездообразно относительно x, то образ f(s) звездообразно относительно f(x).
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \Rightarrow StarConvex_{\mathbb{K}}(f(x), f''s)$$$$
Lean4
theorem starConvex_iff_forall_pos (hx : x ∈ s) :
StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
by
refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
intro h y hy a b ha hb hab
obtain rfl | ha := ha.eq_or_lt
· rw [zero_add] at hab
rwa [hab, one_smul, zero_smul, zero_add]
obtain rfl | hb := hb.eq_or_lt
· rw [add_zero] at hab
rwa [hab, one_smul, zero_smul, add_zero]
exact h hy ha hb hab
