English
If for every point x in s there exists a point y in t with edist x y ≤ r, and conversely for every x in t there exists a y in s with edist x y ≤ r, then the Hausdorff distance between s and t is at most r.
Русский
Если для каждой точки x из множества s существует точка y из множества t такая, что edist x y ≤ r, и наоборот для каждой точки x из t существует y из s с edist x y ≤ r, то расстояние Хаусдорфа между s и t не превышает r.
LaTeX
$$$ (\forall x \in s, \exists y \in t, \operatorname{edist}(x,y) \le r) \to (\forall x \in t, \exists y \in s, \operatorname{edist}(x,y) \le r) \to \operatorname{hausdorffEdist}(s,t) \le r $$$
Lean4
/-- Bounding the Hausdorff edistance by exhibiting, for any point in each set,
another point in the other set at controlled distance -/
theorem hausdorffEdist_le_of_mem_edist {r : ℝ≥0∞} (H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r)
(H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) : hausdorffEdist s t ≤ r :=
by
refine hausdorffEdist_le_of_infEdist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
· rcases H1 x xs with ⟨y, yt, hy⟩
exact le_trans (infEdist_le_edist_of_mem yt) hy
· rcases H2 x xt with ⟨y, ys, hy⟩
exact le_trans (infEdist_le_edist_of_mem ys) hy
