English
The preimage of a star-convex set under an affine map is star-convex.
Русский
Предобраз звёздочно выпуклого множества под аффинным отображением остаётся звёздочно выпуклым.
LaTeX
$$$\\text{StarConvex}_{\\mathbb{K}}(x, s) \\Rightarrow \\text{StarConvex}_{\\mathbb{K}}(x, f^{-1}(s))$, где $f$ — аффинное отображение.$$
Lean4
/-- The preimage of a star-convex set under an affine map is star-convex. -/
theorem affine_preimage (f : E →ᵃ[𝕜] F) {s : Set F} (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (f ⁻¹' s) :=
by
intro y hy a b ha hb hab
rw [mem_preimage, Convex.combo_affine_apply hab]
exact hs hy ha hb hab