affine_image — Mathlib

English

The image of a star-convex set under an affine map is star-convex.

Русский

Образ звёздочно выпуклого множества под аффинным отображением остаётся звёздочно выпуклым.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(x, s) \\Rightarrow \\text{StarConvex}_{\\mathbb{K}}(f(x), f(s))$ для аффинного отображения $f$.$$

Lean4

/-- The image of a star-convex set under an affine map is star-convex. -/
theorem affine_image (f : E →ᵃ[𝕜] F) {s : Set E} (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (f x) (f '' s) :=
  by
  rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab
  refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩
  rw [Convex.combo_affine_apply hab, hy'f]

Похожие утверждения