preimage_add_right — Mathlib

English

Taking the preimage under the map v ↦ v + z preserves star-convexity of the set when shifted by z.

Русский

Образ предобраза при отображении v ↦ v+z сохраняет звездо-выпуклость множества после смещения на z.

LaTeX

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

Lean4

/-- The translation of a star-convex set is also star-convex. -/
theorem preimage_add_right (hs : StarConvex 𝕜 (z + x) s) : StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s) :=
  by
  intro y hy a b ha hb hab
  have h := hs hy ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

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