English
The distance from x to t is at most the distance to s plus the Hausdorff distance between s and t: infEdist x t ≤ infEdist x s + hausdorffEdist s t.
Русский
Расстояние от x до t не больше расстояния от x до s плюс расстояние Хаусдорфа между s и t: infEdist x t ≤ infEdist x s + hausdorffEdist s t.
LaTeX
$$$ \infEdist(x,t) \le \infEdist(x,s) + \operatorname{hausdorffEdist}(s,t) $$$
Lean4
/-- The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
between `s` and `t`. -/
theorem infEdist_le_infEdist_add_hausdorffEdist : infEdist x t ≤ infEdist x s + hausdorffEdist s t :=
ENNReal.le_of_forall_pos_le_add fun ε εpos h =>
by
have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos
have : infEdist x s < infEdist x s + ε / 2 := ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0
obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEdist x s + ↑ε / 2⟩ := infEdist_lt_iff.mp this
have : hausdorffEdist s t < hausdorffEdist s t + ε / 2 := ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0
obtain ⟨z : α, zt : z ∈ t, dyz : edist y z < hausdorffEdist s t + ↑ε / 2⟩ :=
exists_edist_lt_of_hausdorffEdist_lt ys this
calc
infEdist x t ≤ edist x z := infEdist_le_edist_of_mem zt
_ ≤ edist x y + edist y z := (edist_triangle _ _ _)
_ ≤ infEdist x s + ε / 2 + (hausdorffEdist s t + ε / 2) := (add_le_add dxy.le dyz.le)
_ = infEdist x s + hausdorffEdist s t + ε := by simp [ENNReal.add_halves, add_comm, add_left_comm]
