English
Let f: E → F be a linear map over 𝕜. If a set s ⊆ F is star-convex at the point f(x), then its preimage under f is star-convex at x.
Русский
Пусть f: E → F линейное отображение над 𝕜. Если множество s ⊆ F звездообразно выпукло в точке f(x), то его предобраз f⁻¹(s) относительно x также звездообразно выпукло.
LaTeX
$$$\text{If } f: E \to F \text{ is linear and } \mathrm{StarConvex}_{\mathbb{K}}(f(x),s), \text{ then } \mathrm{StarConvex}_{\mathbb{K}}(x,f^{-1}(s)).$$$
Lean4
theorem linear_preimage {s : Set F} (f : E →ₗ[𝕜] F) (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (f ⁻¹' s) :=
by
intro y hy a b ha hb hab
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
exact hs hy ha hb hab
