emetric_closedBall — Mathlib

English

For any ε ≥ 0, closed balls defined via the edistance coincide with ordinary closed balls: EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε.

Русский

Для любого ε ≥ 0 замкнутые шары по edist совпадают с обычными замкнутыми шарами: EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε.

LaTeX

$$$\\forall x\\in α,\\ \\forall ε\\ge 0,\\ EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε.$$$

Lean4

/-- Closed balls defined using the distance or the edistance coincide -/
theorem emetric_closedBall {x : α} {ε : ℝ} (h : 0 ≤ ε) : EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε := by
  ext y; simp [edist_le_ofReal h]

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