add_right — Mathlib

English

Similarly, translating a star-convex set by a fixed vector on the right preserves star-convexity of the image.

Русский

Аналогично: смещение звездо-выпуклого множества справа сохраняет звездную выпуклость образа.

LaTeX

$$$$ \text{StarConvex}(x,s) \Rightarrow \text{StarConvex}(x+z, \{\;s+z\;\}). $$$$

Lean4

theorem add_right (hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (x + z) ((fun x => x + z) '' s) :=
  by
  intro y hy a b ha hb hab
  obtain ⟨y', hy', rfl⟩ := hy
  refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
  match_scalars <;> simp [hab]

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