edist_lt_ofReal — Mathlib

English

Let α be a pseudo-metric space. For all x, y ∈ α and all real r, the strict inequality edist x y < ENNReal.ofReal r holds if and only if dist x y < r.

Русский

Пусть α является псевдометрическим пространством. Для любых x, y ∈ α и любого действительного r верно: edist x y < ENNReal.ofReal r тогда и только тогда, dist x y < r.

LaTeX

$$$ \forall x,y$ in $\alpha$, $r \in \mathbb{R}$, \\ edist x y < \operatorname{ENNReal.ofReal} r \ \Longleftrightarrow \ dist x y < r$$$

Lean4

@[simp]
theorem edist_lt_ofReal {x y : α} {r : ℝ} : edist x y < ENNReal.ofReal r ↔ dist x y < r := by
  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]

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