emetric_ball_nnreal — Mathlib

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

Похожие утверждения