edist_le_ofReal — Mathlib

English

Let α be a pseudo-metric space. If r ≥ 0, then edist x y ≤ ENNReal.ofReal r iff dist x y ≤ r.

Русский

Пусть α является псевдометрическим пространством. При r ≥ 0 выполняется: edist x y ≤ ENNReal.ofReal r ⇔ dist x y ≤ r.

LaTeX

$$$ \forall x,y \in \alpha,\; (0 \le r) \Rightarrow edist x y \le \operatorname{ENNReal.ofReal} r \iff dist x y \le r$$$

Lean4

@[simp]
theorem edist_le_ofReal {x y : α} {r : ℝ} (hr : 0 ≤ r) : edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r := by
  rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

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