of_pairwise_sphere_norm_ne_two — Mathlib

English

If the unit sphere is pairwise such that for any two distinct points x,y on the sphere we have ∥x+y∥ ≠ 2, then the space is strictly convex.

Русский

Если на единичной сфере для любых двух различных точек x,y выполняется ∥x+y∥ ≠ 2, то пространство строго выпукло.

LaTeX

$$$\bigl(\forall x,y\in \mathbb{S}(0,1), x\neq y \Rightarrow \|x+y\| \neq 2\bigr) \Rightarrow \ StrictConvexSpace_{\mathbb{R}} E$$$

Lean4

theorem of_pairwise_sphere_norm_ne_two (h : (sphere (0 : E) 1).Pairwise fun x y => ‖x + y‖ ≠ 2) :
    StrictConvexSpace ℝ E :=
  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy =>
    h (mem_sphere_zero_iff_norm.2 hx) (mem_sphere_zero_iff_norm.2 hy)

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