English
Bounding hausdorffDist by infDist: if for all x ∈ s, infDist(x, t) ≤ r and for all x ∈ t, infDist(x, s) ≤ r, then hausdorffDist(s, t) ≤ r.
Русский
Границы расстояния Хаусдорфа по infDist: если для всех x ∈ s верно infDist(x, t) ≤ r и для всех x ∈ t верно infDist(x, s) ≤ r, то hausdorffDist(s,t) ≤ r.
LaTeX
$$$\text{If } r\ge0,\ (\forall x\in s,\infDist(x,t)\le r)\ \land\ (\forall x\in t,\infDist(x,s)\le r)\Rightarrow \operatorname{hausdorffDist}(s,t)\le r.$$$
Lean4
/-- Bounding the Hausdorff distance by bounding the distance of any point
in each set to the other set -/
theorem hausdorffDist_le_of_infDist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, infDist x t ≤ r)
(H2 : ∀ x ∈ t, infDist x s ≤ r) : hausdorffDist s t ≤ r :=
by
rcases s.eq_empty_or_nonempty with hs | hs
· rwa [hs, hausdorffDist_empty']
rcases t.eq_empty_or_nonempty with ht | ht
· rwa [ht, hausdorffDist_empty]
have : hausdorffEdist s t ≤ ENNReal.ofReal r :=
by
apply hausdorffEdist_le_of_infEdist _ _
· simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top ht) hr] using H1
· simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top hs) hr] using H2
exact ENNReal.toReal_le_of_le_ofReal hr this
