English
If a set s in E×E is star-convex at the point (x,y), then the image of s under the map (u,v) ↦ u − v is star-convex at x − y.
Русский
Если множество s в E×E звёздочно выпукло относительно точки (x,y), то образ этого множества под отображением (u,v) ↦ u − v звёздочно выпукл относительно точки x − y.
LaTeX
$$$\\text{StarConvex}_{\\mathbb{K}}({\\text{fst}}=x, {\\text{snd}}=y)\\; s \\Rightarrow\\; \\text{StarConvex}_{\\mathbb{K}}(x-y, \\{u-v : (u,v)\\in s\\})$$$
Lean4
theorem sub' {s : Set (E × E)} (hs : StarConvex 𝕜 (x, y) s) :
StarConvex 𝕜 (x - y) ((fun x : E × E => x.1 - x.2) '' s) :=
hs.is_linear_image IsLinearMap.isLinearMap_sub
