volume_emetric_closedBall — Mathlib

English

For a ∈ ℝ and r ∈ ℝ≥0∞, the volume of the EMetric closed ball is 2r.

Русский

Для a ∈ ℝ и r ∈ ℝ≥0∞ объем EMetric замкнутого шара равен 2r.

LaTeX

$$$\operatorname{volume}(\mathrm{EMetric.closedBall}(a,r)) = 2r$$$

Lean4

@[simp]
theorem volume_emetric_closedBall (a : ℝ) (r : ℝ≥0∞) : volume (EMetric.closedBall a r) = 2 * r :=
  by
  rcases eq_or_ne r ∞ with (rfl | hr)
  · rw [EMetric.closedBall_top, volume_univ, two_mul, _root_.top_add]
  · lift r to ℝ≥0 using hr
    rw [Metric.emetric_closedBall_nnreal, volume_closedBall, two_mul, ← NNReal.coe_add, ENNReal.ofReal_coe_nnreal,
      ENNReal.coe_add, two_mul]

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