English
If x,y lie in a closed ball around z with radius r, x ≠ y, and a,b>0 with a+b=1, then the convex combination a x + b y lies in the open ball (radius r).
Русский
Если x,y лежат в замкнутом шаре вокруг z радиуса r, x ≠ y, и коэффициенты a,b>0 с a+b=1, то сумма взвешенная a x + b y принадлежит открытой шару вокруг z.
LaTeX
$$$x,y\in \overline{B}(z,r), x\neq y, a>0, b>0, a+b=1 \Rightarrow a\,x + b\,y \in B(z,r).$$$
Lean4
/-- If `x ≠ y` belong to the same closed ball, then a convex combination of `x` and `y` with
positive coefficients belongs to the corresponding open ball. -/
theorem combo_mem_ball_of_ne (hx : x ∈ closedBall z r) (hy : y ∈ closedBall z r) (hne : x ≠ y) (ha : 0 < a) (hb : 0 < b)
(hab : a + b = 1) : a • x + b • y ∈ ball z r :=
by
rcases eq_or_ne r 0 with (rfl | hr)
· rw [closedBall_zero, mem_singleton_iff] at hx hy
exact (hne (hx.trans hy.symm)).elim
· simp only [← interior_closedBall _ hr] at hx hy ⊢
exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab
