English
If the unit sphere is pairwise such that the sum of any two distinct points on the sphere does not lie on the sphere (i.e., ∥x+y∥ ≠ 2 for x≠y on the unit sphere), then the space is strictly convex.
Русский
Если парность на единичной сфере обеспечивает несуществование равенства для суммы двух различных векторов, то пространство строго строго выпукло.
LaTeX
$$$\bigl((\mathbb{S}(0,1)).\text{Pairwise }(\|x+y\| \neq 2)\bigr) \Rightarrow \ StrictConvexSpace_{\mathbb{R}} E$$$
Lean4
theorem of_norm_combo_ne_one
(h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) :
StrictConvexSpace ℝ E :=
by
refine StrictConvexSpace.of_strictConvex_unitClosedBall ℝ ((convex_closedBall _ _).strictConvex ?_)
simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise, frontier_closedBall _ one_ne_zero,
mem_sphere_zero_iff_norm]
intro x hx y hy hne
rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩
exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩
