English
If s and t are nonempty and bounded in a metric space, their Hausdorff distance is finite.
Русский
Если множества s и t не пусты и ограничены в метрическом пространстве, расстояние Хаусдорфа ограничено сверху (конечное).
LaTeX
$$$\operatorname{hausdorffEdist}(s,t) \neq \top.$$$
Lean4
/-- If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff
edistance. -/
theorem hausdorffEdist_ne_top_of_nonempty_of_bounded (hs : s.Nonempty) (ht : t.Nonempty) (bs : IsBounded s)
(bt : IsBounded t) : hausdorffEdist s t ≠ ⊤ :=
by
rcases hs with ⟨cs, hcs⟩
rcases ht with ⟨ct, hct⟩
rcases bs.subset_closedBall ct with ⟨rs, hrs⟩
rcases bt.subset_closedBall cs with ⟨rt, hrt⟩
have : hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt) :=
by
apply hausdorffEdist_le_of_mem_edist
· intro x xs
exists ct, hct
have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
exact le_trans dist_nonneg this
· intro x xt
exists cs, hcs
have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
exact le_trans dist_nonneg this
exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top this
