English
If hs is star-convex at x with respect to a set s and f is linear, then the image of s under f is star-convex at f(x).
Русский
Если s звездообразно относительно x, и f линейно, то образ s под действием f звездообразен относительно f(x).
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \Rightarrow StarConvex_{\mathbb{K}}(f(x), f''s).$$$$
Lean4
theorem is_linear_image (hs : StarConvex 𝕜 x s) {f : E → F} (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 (f x) (f '' s) :=
hs.linear_image <| hf.mk' f