ball_disjoint — Mathlib

English

If ε1 + ε2 ≤ edist(x,y), then the balls B(x,ε1) and B(y,ε2) are disjoint.

Русский

Если ε1 + ε2 ≤ edist(x,y), то шары B(x,ε1) и B(y,ε2) не пересекаются.

LaTeX

$$$\\mathrm{ball}(x,\\varepsilon_1) \\cap \\mathrm{ball}(y,\\varepsilon_2) = \\emptyset \\quad \\text{whenever } \\varepsilon_1 + \\varepsilon_2 \\le \\operatorname{edist}(x,y)$$$

Lean4

theorem ball_disjoint (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (ball x ε₁) (ball y ε₂) :=
  Set.disjoint_left.mpr fun z h₁ h₂ => (edist_triangle_left x y z).not_gt <| (ENNReal.add_lt_add h₁ h₂).trans_le h

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