volume_closedBall_fin_three — Mathlib

English

In E = R^3, the volume of the closed ball of radius r is (4/3) π r^3.

Русский

В R^3 объём замкнутого шара радиуса r равен (4/3) π r^3.

LaTeX

$$$$ \operatorname{vol}(\overline{B}(x,r)) = \dfrac{4}{3} \pi r^{3} $$$$

Lean4

@[simp]
theorem volume_closedBall_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ 3 * .ofReal (π * 4 / 3) := by
  rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_three x]

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