English
Balls defined via the distance and via the edistance coincide: for any x and any ε ∈ ℝ, EMetric.ball x (ENNReal.ofReal ε) = ball x ε.
Русский
Шары, определяемые через расстояние и через edist совпадают: для любых x и ε ∈ ℝ, EMetric.ball x(ENNReal.ofReal ε) = ball x ε.
LaTeX
$$$\\forall x\\in α, \\forall ε\\in \\mathbb{R},\\ EMetric.ball(x,\\operatorname{ENNReal.ofReal} ε) = \\operatorname{ball}(x, ε).$$$
Lean4
/-- Balls defined using the distance or the edistance coincide -/
@[simp]
theorem emetric_ball {x : α} {ε : ℝ} : EMetric.ball x (ENNReal.ofReal ε) = ball x ε :=
by
ext y
simp only [EMetric.mem_ball, mem_ball, edist_dist]
exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg