volume_real_closedBall — Mathlib

English

If r ≥ 0, then the real-valued volume of the closed ball of radius r around a is 2r.

Русский

Если r ≥ 0, то действительный объем замкнутого шара радиуса r вокруг a равен 2r.

LaTeX

$$$0 \le r \Rightarrow \operatorname{volume.real}(\mathrm{closedBall}(a,r)) = 2r$$$

Lean4

@[simp]
theorem volume_real_closedBall {a r : ℝ} (hr : 0 ≤ r) : volume.real (Metric.closedBall a r) = 2 * r := by
  simp [measureReal_def, hr]

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