English
Let E be a normed real vector space. If hδ ≥ 0 and hε ≥ 0, then Disjoint(closedBall x δ, closedBall y ε) holds if and only if δ+ε < dist(x,y).
Русский
Пусть E — нормированное вещественное векторное пространство. Пусть δ≥0 и ε≥0. Тогда замкнутые шары по-прежнему не пересекаются тогда и только тогда, когда δ+ε < dist(x,y).
LaTeX
$$$$\forall x,y \in E,\forall δ,ε \ge 0:\; \operatorname{Disjoint}(\operatorname{closedBall}(x,δ), \operatorname{closedBall}(y,ε)) \iff δ+ε < dist(x,y). $$$$
Lean4
theorem disjoint_closedBall_closedBall_iff (hδ : 0 ≤ δ) (hε : 0 ≤ ε) :
Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y :=
by
refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩
rw [add_comm] at hxy
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
rw [dist_comm] at hxz
exact h.le_bot ⟨hxz, hzy⟩
