disjoint_closedBall_of_lt_infEdist

English

If r < infEdist x s, then the closed ball centered at x with radius r is disjoint from s.

Русский

Если r < infEdist x s, то замкнутый шар B̄(x,r) не пересекает s.

LaTeX

$$$\text{If } r < \infEdist x s\text{ then } \operatorname{Disjoint}(\overline{B}(x,r), s)$$$

Lean4

theorem disjoint_closedBall_of_lt_infEdist {r : ℝ≥0∞} (h : r < infEdist x s) : Disjoint (closedBall x r) s :=
  by
  rw [disjoint_left]
  intro y hy h'y
  apply lt_irrefl (infEdist x s)
  calc
    infEdist x s ≤ edist x y := infEdist_le_edist_of_mem h'y
    _ ≤ r := by rwa [mem_closedBall, edist_comm] at hy
    _ < infEdist x s := h

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