English
Let E be a normed real vector space. If hδ > 0 and hε ≥ 0, then Disjoint(ball x δ, closedBall y ε) holds if and only if δ+ε ≤ dist(x,y).
Русский
Пусть E — нормированное вещественное векторное пространство. Если δ>0 и ε≥0, то ball(x,δ) и closedBall(y,ε) непересекаются тогда и только тогда, когда δ+ε ≤ dist(x,y).
LaTeX
$$$$\forall x,y \in E,\forall δ>0, ε\ge 0:\; \operatorname{Disjoint}(\operatorname{ball}(x,δ), \operatorname{closedBall}(y,ε)) \iff δ+ε \le dist(x,y). $$$$
Lean4
theorem disjoint_ball_closedBall_iff (hδ : 0 < δ) (hε : 0 ≤ ε) :
Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y :=
by
refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩
rw [add_comm] at hxy
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy
rw [dist_comm] at hxz
exact
h.le_bot
⟨hxz, hzy⟩
-- This is also true for `ℚ`-normed spaces
