emetric_closedBall_nnreal — Mathlib

English

For radii ε ∈ ℝ≥0, the edistance closed ball equals the ordinary closed ball: EMetric.closedBall x (ENNReal.ofNNReal ε) = closedBall x ε.

Русский

Для ε ∈ ℝ≥0, замкнутый шар по edist совпадает с обычным замкнутым шаром: EMetric.closedBall x (ENNReal.ofNNReal ε) = closedBall x ε.

LaTeX

$$$\\forall x\\in α,\\ EMetric.closedBall x (ENNReal.ofNNReal ε) = closedBall x ε.$$$

Lean4

/-- Closed balls defined using the distance or the edistance coincide -/
@[simp]
theorem emetric_closedBall_nnreal {x : α} {ε : ℝ≥0} : EMetric.closedBall x ε = closedBall x ε := by
  rw [← Metric.emetric_closedBall ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

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