disjoint_ball_infDist — Mathlib

English

If r is strictly smaller than infDist(x, s), then the closed ball centered at x with radius r is disjoint from s.

Русский

Если r < infDist(x, s), то закрытый шар вокруг x радиуса r не пересекает s.

LaTeX

$${r ∈ \mathbb{R}} (r < \infDist x s) \Rightarrow Disjoint(ClosedBall(x,r), s)$$

Lean4

theorem disjoint_ball_infDist : Disjoint (ball x (infDist x s)) s :=
  disjoint_left.2 fun _y hy => notMem_of_dist_lt_infDist <| mem_ball'.1 hy

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