add_left — Mathlib

English

Translating a star-convex set by a fixed vector on the left preserves star-convexity of the image.

Русский

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

LaTeX

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

Lean4

theorem add_left (hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (z + x) ((fun x => z + x) '' 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]

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