Open_Ball_of_Point_Inside_Open_Ball
Provedopen-ballsproofwiki
Let be a metric space. Let be an open -ball in . Let . Then That is, for every point in an open -ball in a metric space, there exists an open -ball of that point entirely contained within that open -ball.
Preamble
import Mathlib.Topology.MetricSpace.Basic
Formal statement
theorem Open_Ball_of_Point_Inside_Open_Ball {α : Type _} [PseudoMetricSpace α] (x y : α) (ε : ℝ) (hy : y ∈ Metric.ball x ε) : ∃ δ > 0, Metric.ball y δ ⊆ Metric.ball x ε := by sorrySource