affinity — Mathlib

English

If s is star-convex at x, then for any z∈E and c∈𝕜, the set image under w ↦ z + c w is star-convex at z + c x.

Русский

Если s звёздочно выпукло относительно x, то образ под отображением w ↦ z + c w звёздочно выпукл относительно z + c x.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(x, s) \\Rightarrow \\forall z,c,\\ \\text{StarConvex}_{\\mathbb{K}}(z + c x, \\{z + c w : w\\in s\\})$$$

Lean4

theorem affinity (hs : StarConvex 𝕜 x s) (z : E) (c : 𝕜) : StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s) :=
  by
  have h := (hs.smul c).add_left z
  rwa [← image_smul, image_image] at h

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