English
For radii ε in ℝ≥0 (nonnegative), the edistance ball equals the metric ball: EMetric.ball x ε = ball x ε.
Русский
Для радиусов ε ∈ ℝ≥0 (неотрицательных) шар по edist совпадает с обычным шаром: EMetric.ball x ε = ball x ε.
LaTeX
$$$\\forall x\\in α,\\ \\forall ε\\in\\mathbb{R}_{≥0},\\ EMetric.ball x (ENNReal.ofNNReal ε) = ball x ε.$$$
Lean4
/-- Balls defined using the distance or the edistance coincide -/
@[simp]
theorem emetric_ball_nnreal {x : α} {ε : ℝ≥0} : EMetric.ball x ε = ball x ε :=
by
rw [← Metric.emetric_ball]
simp