volume_emetric_ball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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