closedBall_disjoint_closedBall — Mathlib

English

If δ + ε < dist x y, then the closed balls around x and y are disjoint.

Русский

Если δ + ε < расстояние между x и y, тогда замкнутые шары вокруг x и y не пересекаются.

LaTeX

$$δ + ε < dist(x,y) ⇒ Disjoint(closedBall(x,δ), closedBall(y,ε))$$

Lean4

theorem closedBall_disjoint_closedBall (h : δ + ε < dist x y) : Disjoint (closedBall x δ) (closedBall y ε) :=
  Set.disjoint_left.mpr fun _a ha1 ha2 => h.not_ge <| (dist_triangle_left _ _ _).trans <| add_le_add ha1 ha2

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