openSegment_subset_ball_of_ne — Mathlib

English

If norms satisfy ≤ r and x ≠ y with a,b>0 and a+b=1, then the convex combination a x + b y lies strictly inside the ball of radius r.

Русский

Если нормы удовлетворяют ≤ r и x ≠ y, а коэффициенты a,b>0 и a+b=1, то выпуклая комбинация a x + b y лежит строго внутри шара радиуса r.

LaTeX

$$$\|x\| \le r,\ \|y\| \le r,\ x \neq y,\ a>0,\ b>0,\ a+b=1 \Rightarrow \|a x + b y\| < r$$$

Lean4

/-- If `x ≠ y` belong to the same closed ball, then the open segment with endpoints `x` and `y` is
included in the corresponding open ball. -/
theorem openSegment_subset_ball_of_ne (hx : x ∈ closedBall z r) (hy : y ∈ closedBall z r) (hne : x ≠ y) :
    openSegment ℝ x y ⊆ ball z r :=
  (openSegment_subset_iff _).2 fun _ _ => combo_mem_ball_of_ne hx hy hne

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