English
If x ∈ s and the Hausdorff distance between s and t is finite, then infDist(x, t) ≤ hausdorffDist(s, t).
Русский
Если x ∈ s и расстояние Хаусдорфа между s и t конечно, то infDist(x, t) ≤ hausdorffDist(s, t).
LaTeX
$$$\text{If } x\in s \text{ and } \operatorname{hausdorffEdist}(s,t)\neq \top,\ \infDist(x,t) \le \operatorname{hausdorffDist}(s,t).$$$
Lean4
/-- The Hausdorff distance is controlled by the diameter of the union. -/
theorem hausdorffDist_le_diam (hs : s.Nonempty) (bs : IsBounded s) (ht : t.Nonempty) (bt : IsBounded t) :
hausdorffDist s t ≤ diam (s ∪ t) := by
rcases hs with ⟨x, xs⟩
rcases ht with ⟨y, yt⟩
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_
· exact fun z hz => ⟨y, yt, dist_le_diam_of_mem (bs.union bt) (subset_union_left hz) (subset_union_right yt)⟩
· exact fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz) (subset_union_left xs)⟩
