edist_lt_top — Mathlib

English

In a pseudometric space, the extended distance is always finite: edist(x,y) < ⊤.

Русский

В псевдометрическом пространстве расширенное расстояние всегда конечное: edist(x,y) < ⊤.

LaTeX

$$edist(x,y) < \top$$

Lean4

/-- In a pseudometric space, the extended distance is always finite -/
theorem edist_lt_top {α : Type*} [PseudoMetricSpace α] (x y : α) : edist x y < ⊤ :=
  (edist_dist x y).symm ▸ ENNReal.ofReal_lt_top

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