Distinct_Points_in_Metric_Space_have_Disjoint_Open_Balls

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

open-ballsproofwiki

Let $M = \left({A, d}\right)$ be a metric space. Let $x, y \in M: x \ne y$ . Then there exist disjoint open $\epsilon$ -balls $B_\epsilon \left({x}\right)$ and $B_\epsilon \left({y}\right)$ containing $x$ and $y$ respectively.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Distinct_Points_in_Metric_Space_have_Disjoint_Open_Balls {α : Type _} [MetricSpace α] (x y : α) (hxy : x ≠ y) : ∃ r₁ r₂ : ℝ, r₁ > 0 ∧ r₂ > 0 ∧ Disjoint (Metric.ball x r₁) (Metric.ball y r₂) := by sorry

Source

https://proofwiki.org/wiki/Distinct_Points_in_Metric_Space_have_Disjoint_Open_Balls

View graph