English
For closed sets s,t, the edistance equals the Hausdorff distance between them.
Русский
Расстояние между замкнутыми множествами s и t равно расстоянию Гаусдорфа между ними.
LaTeX
$$$\\operatorname{edist}(s,t) = \\operatorname{hausdorffEdist}(s,t).$$$
Lean4
/-- The edistance to a closed set depends continuously on the point and the set -/
theorem continuous_infEdist_hausdorffEdist : Continuous fun p : α × Closeds α => infEdist p.1 p.2 :=
by
refine continuous_of_le_add_edist 2 (by simp) ?_
rintro ⟨x, s⟩ ⟨y, t⟩
calc
infEdist x s ≤ infEdist x t + hausdorffEdist (t : Set α) s := infEdist_le_infEdist_add_hausdorffEdist
_ ≤ infEdist y t + edist x y + hausdorffEdist (t : Set α) s := by gcongr; apply infEdist_le_infEdist_add_edist
_ = infEdist y t + (edist x y + hausdorffEdist (s : Set α) t) := by rw [add_assoc, hausdorffEdist_comm]
_ ≤ infEdist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) := by
gcongr <;> apply_rules [le_max_left, le_max_right]
_ = infEdist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]
