edist_ne_top_of_mem_ball — Mathlib

English

In an extended metric space, the distance between two points inside an emetric ball is finite.

Русский

Расстояние между любыми двумя точками внутри шаровой области в эметрическом пространстве конечное.

LaTeX

$$$\edist x y \neq \infty$ для любых $x,y$ внутри эпсилон-окрестности шарa.$$

Lean4

/-- In an emetric ball, the distance between points is everywhere finite -/
theorem edist_ne_top_of_mem_ball {a : β} {r : ℝ≥0∞} (x y : ball a r) : edist x.1 y.1 ≠ ∞ :=
  ne_of_lt <|
    calc
      edist x y ≤ edist a x + edist a y := edist_triangle_left x.1 y.1 a
      _ < r + r := by rw [edist_comm a x, edist_comm a y]; exact ENNReal.add_lt_add x.2 y.2
      _ ≤ ∞ := le_top

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