infDist_le_infDist_add_dist — Mathlib

English

The open ball centered at x with radius infDist(x, s) is disjoint from s.

Русский

Открытый шар с центром в x и радиусом infDist(x, s) не перекрывается с s.

LaTeX

$$Disjoint( Ball(x, infDist(x, s)) , s )$$

Lean4

/-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
the distance between `x` and `y`. -/
theorem infDist_le_infDist_add_dist : infDist x s ≤ infDist y s + dist x y :=
  by
  rw [infDist, infDist, dist_edist]
  refine ENNReal.toReal_le_add' infEdist_le_infEdist_add_edist ?_ (flip absurd (edist_ne_top _ _))
  simp only [infEdist_eq_top_iff, imp_self]

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