emetric_ball — Mathlib

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

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