infEdist_le_infEdist_add_edist — Mathlib

English

For any x, y and set s, infEdist x s ≤ infEdist y s + edist x y.

Русский

Для любых x, y и множества s верно: infEdist x s ≤ infEdist y s + edist x y.

LaTeX

$$$\infEdist x s \le \infEdist y s + edist x y$$$

Lean4

/-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
the edist from `x` to `y` -/
theorem infEdist_le_infEdist_add_edist : infEdist x s ≤ infEdist y s + edist x y :=
  calc
    ⨅ z ∈ s, edist x z ≤ ⨅ z ∈ s, edist y z + edist x y :=
      iInf₂_mono fun _ _ => (edist_triangle _ _ _).trans_eq (add_comm _ _)
    _ = (⨅ z ∈ s, edist y z) + edist x y := by simp only [ENNReal.iInf_add]

Похожие утверждения