English
Bounding hausdorffDist by pointwise distances: if for all x ∈ s there exists y ∈ t with dist(x,y) ≤ r, and for all x ∈ t there exists y ∈ s with dist(x,y) ≤ r, then hausdorffDist(s,t) ≤ r.
Русский
Границы hausdorffDist по точечным расстояниям: если для каждой x ∈ s существует y ∈ t с dist(x,y) ≤ r и для каждой x ∈ t существует y ∈ s с dist(x,y) ≤ r, то hausdorffDist(s,t) ≤ r.
LaTeX
$$$\forall r\ge0,\ (\forall x\in s,\exists y\in t,\operatorname{dist}(x,y)\le r)\ \land\ (\forall x\in t,\exists y\in s,\operatorname{dist}(x,y)\le r)\Rightarrow \operatorname{hausdorffDist}(s,t)\le r.$$$
Lean4
/-- Bounding the Hausdorff distance by exhibiting, for any point in each set,
another point in the other set at controlled distance -/
theorem hausdorffDist_le_of_mem_dist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r)
(H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) : hausdorffDist s t ≤ r :=
by
apply hausdorffDist_le_of_infDist hr
· intro x xs
rcases H1 x xs with ⟨y, yt, hy⟩
exact le_trans (infDist_le_dist_of_mem yt) hy
· intro x xt
rcases H2 x xt with ⟨y, ys, hy⟩
exact le_trans (infDist_le_dist_of_mem ys) hy
