edist_ne_top — Mathlib

English

Edist between any two points is not equal to the top element: edist(x,y) ≠ ⊤.

Русский

Расстояние edist между любыми двумя точками не равно верхней границе: edist(x,y) ≠ ⊤.

LaTeX

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

Lean4

/-- In a pseudometric space, the extended distance is always finite -/
@[aesop (rule_sets := [finiteness]) safe apply]
theorem edist_ne_top (x y : α) : edist x y ≠ ⊤ :=
  (edist_lt_top x y).ne

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