English
If s is star-convex at f(x) for some map f, and f is an arbitrary linear map (IsLinearMap), then s preimage under f is star-convex at x.
Русский
Если множество s звездообразно выпукло относительно f(x) для некоторого отображения f и f является линейным отображением, то предобраз s под f выпукло звездообразно в x.
LaTeX
$$$\text{If } hs: \mathrm{StarConvex}_{\mathbb{K}}(f(x),s) \text{ and } hf: \mathrm{IsLinearMap}_{\mathbb{K}}(f), \text{ then } \mathrm{StarConvex}_{\mathbb{K}}(x, f^{-1}(s)).$$$
Lean4
theorem is_linear_preimage {s : Set F} {f : E → F} (hs : StarConvex 𝕜 (f x) s) (hf : IsLinearMap 𝕜 f) :
StarConvex 𝕜 x (preimage f s) :=
hs.linear_preimage <| hf.mk' f