edist_le_infEdist_add_ediam — Mathlib

English

If y ∈ s, then edist x y ≤ infEdist x s + diam s.

Русский

Если y ∈ s, то edist x y ≤ infEdist x s + diam s.

LaTeX

$$$\forall x\forall y\,(y \in s \Rightarrow edist x y \le infEdist x s + diam s)$$$

Lean4

theorem edist_le_infEdist_add_ediam (hy : y ∈ s) : edist x y ≤ infEdist x s + diam s :=
  by
  simp_rw [infEdist, ENNReal.iInf_add]
  refine le_iInf₂ fun i hi => ?_
  calc
    edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
    _ ≤ edist x i + diam s := add_le_add le_rfl (edist_le_diam_of_mem hi hy)

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