vadd — Mathlib

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

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