affine_preimage — Mathlib

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

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