Closure_of_Open_Ball_in_Metric_Space
Provedopen-ballsproofwiki
Let be a metric space. Let be an open -ball in . Let , where denotes the closure of . Then .
Preamble
import Mathlib.Topology.MetricSpace.Basic
Formal statement
theorem Closure_of_Open_Ball_in_Metric_Space {α : Type _} [PseudoMetricSpace α] (x : α) (r : ℝ) : closure (Metric.ball x r) ⊆ Metric.closedBall x r := by sorrySource