add_left — Mathlib

English

Translating a strictly convex set by z preserves strict convexity of the image.

Русский

Перемещение множества по z сохраняет строгое выпуклое образ.

LaTeX

$$$StrictConvex 𝕜 s \Rightarrow \forall z:\ E, StrictConvex 𝕜 (Set.image (fun x => x + z) s)$$$

Lean4

theorem add_left (hs : StrictConvex 𝕜 s) (z : E) : StrictConvex 𝕜 ((fun x => z + x) '' s) := by
  simpa only [singleton_add] using (strictConvex_singleton z).add hs

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