volume_ball_fin_three — Mathlib

English

In Euclidean space R^3, the volume of a ball of radius r is (4/3) π r^3.

Русский

В трёхмерном евклидовом пространстве объём сферы радиуса r равен (4/3) π r^3.

LaTeX

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

Lean4

@[simp]
theorem volume_ball_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) :
    volume (ball x r) = .ofReal r ^ 3 * .ofReal (π * 4 / 3) := by
  norm_num [InnerProductSpace.volume_ball_of_dim_odd (k := 1) (by simp) x]

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