English
If two points x,y lie in a closed ball, then the open segment connecting x and y is contained in the open ball, provided x ≠ y and the ball has radius r>0; this follows from strict convexity of the ball.
Русский
Если две точки лежат в замкнутом шарe, то открытый отрезок между ними содержится во внутренности шара, если x ≠ y и радиус положителен; следует из строгой выпуклости шара.
LaTeX
$$$(x,y,z)\text{ с } x,y\in \overline{B}(z,r), x\neq y \Rightarrow \text{openSegment}(x,y)\subset \mathrm{Ball}(z,r)$$$
Lean4
/-- If `‖x + y‖ = ‖x‖ + ‖y‖` implies that `x y : E` are in the same ray, then `E` is a strictly
convex space. See also a more -/
theorem of_norm_add (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) : StrictConvexSpace ℝ E :=
by
refine StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => ?_
rw [mem_sphere_zero_iff_norm] at hx hy
exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)
