disjoint_closedBall_ball_iff — Mathlib

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_ball_iff (hδ : 0 ≤ δ) (hε : 0 < ε) :
    Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y := by
  rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]

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