English
If S is strictly convex, then its translation by any vector x, i.e., x +ᵥ S, is strictly convex.
Русский
Если S строго выпукло, то его перенос на любой вектор x, то есть x +ᵥ S, также строго выпукл.
LaTeX
$$$\StrictConvex 𝕜 s \Rightarrow \StrictConvex 𝕜 (x +ᵥ s)$$$
Lean4
/-- The translation of a strictly convex set is also strictly convex. -/
theorem vadd (hs : StrictConvex 𝕜 s) (x : E) : StrictConvex 𝕜 (x +ᵥ s) :=
hs.add_left x