volume_closedBall — Mathlib

English

Let a ∈ ℝ and r ∈ ℝ. The volume of the closed ball of radius r around a is 2r (via the usual length measure).

Русский

Пусть a ∈ ℝ и r ∈ ℝ. Объем замкнутого шара радиуса r вокруг a равен 2r (по обычному измерению длины).

LaTeX

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

Lean4

@[simp]
theorem volume_closedBall (a r : ℝ) : volume (Metric.closedBall a r) = ofReal (2 * r) := by
  rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]

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