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