English
The infimum distance to s and t are the same, up to the Hausdorff distance: infDist x t ≤ infDist x s + hausdorffDist s t.
Русский
infDist x t не превосходит infDist x s плюс hausdorffDist s t.
LaTeX
$$$\infDist(x,t) \le \infDist(x,s) + \operatorname{hausdorffDist}(s,t).$$$
Lean4
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance
`< r` of a point in the other set. -/
theorem exists_dist_lt_of_hausdorffDist_lt {r : ℝ} (h : x ∈ s) (H : hausdorffDist s t < r)
(fin : hausdorffEdist s t ≠ ⊤) : ∃ y ∈ t, dist x y < r :=
by
have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
have : hausdorffEdist s t < ENNReal.ofReal r := by
rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0), ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
rcases exists_edist_lt_of_hausdorffEdist_lt h this with ⟨y, hy, yr⟩
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr
exact ⟨y, hy, yr⟩
