add_right — Mathlib

English

Let S be a strictly convex subset of a vector space E over 𝕜. For any z ∈ E, the translate z + S is strictly convex.

Русский

Пусть S — строго выпуклое множество векторного пространства E над 𝕜. Для любого z ∈ E сдвиг z + S также является строго выпуклым.

LaTeX

$$$\StrictConvex 𝕜 s \Rightarrow \StrictConvex 𝕜 (z + s)$$$

Lean4

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

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