English
Let E be a vector space and s a star-convex set with respect to a scalar ring 𝕜. If the translate of x by z makes the set s star-convex about x+z, then the preimage of s under the translation by z is star-convex about x.
Русский
Пусть E — векторное пространство, s — звёздочно-выпуктое множество относительно кольца 𝕜. Если перевод множества s на вектор z делает множество звёздочно-выпуклым относительно точки x+z, то множество, взятое как предобраз \(s\) по отображению \(t \mapsto t+z\), звёздочно выпукло относительно x.
LaTeX
$$$\\StarConvex_{\\mathbb{K}}(x, ((t \\mapsto t + z)^{-1} \\, s)),$ где $((t \\mapsto t + z)^{-1} s)=\\{u\\in E : u+z \\in s\\}$$$
Lean4
/-- The translation of a star-convex set is also star-convex. -/
theorem preimage_add_left (hs : StarConvex 𝕜 (x + z) s) : StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s) :=
by
rw [add_comm] at hs
simpa only [add_comm] using hs.preimage_add_right
