Half sums in normed spaces over ℝ or ℂ

In a normed space over an RCLike field, half the sum of two vectors of norm at most B has norm at most B: the closed ball of radius B contains the midpoint of any two of its points.

theorem TauCeti.norm_two_inv_smul_add_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : E} {B : ℝ} (ha : ‖a‖ ≤ B) (hb : ‖b‖ ≤ B) : ‖2⁻¹ • (a + b)‖ ≤ B

Half the sum of two vectors of norm at most B has norm at most B.