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]