English
If s and t are nonempty, then the Hausdorff distance between s and t is at most the diameter of their union.
Русский
Если s и t непусты, то расстояние Хаусдорфа между ними не превосходит диаметр объединения s ∪ t.
LaTeX
$$$ s \neq \varnothing \land t \neq \varnothing \Rightarrow \operatorname{hausdorffEdist}(s,t) \le \operatorname{diam}(s \cup t) $$$
Lean4
/-- The Hausdorff distance is controlled by the diameter of the union. -/
theorem hausdorffEdist_le_ediam (hs : s.Nonempty) (ht : t.Nonempty) : hausdorffEdist s t ≤ diam (s ∪ t) :=
by
rcases hs with ⟨x, xs⟩
rcases ht with ⟨y, yt⟩
refine hausdorffEdist_le_of_mem_edist ?_ ?_
· intro z hz
exact ⟨y, yt, edist_le_diam_of_mem (subset_union_left hz) (subset_union_right yt)⟩
· intro z hz
exact ⟨x, xs, edist_le_diam_of_mem (subset_union_right hz) (subset_union_left xs)⟩
