volume_ball_fin_two — Mathlib

English

In Euclidean plane E = R^2, the volume (area) of a ball of radius r is π r^2.

Русский

В евклидовом пространстве R^2 площадь круга радиуса r равна π r^2.

LaTeX

$$$$ \operatorname{vol}(\text{ball}(x,r)) = r^{2} \cdot \pi $$$$

Lean4

@[simp]
theorem volume_ball_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : volume (ball x r) = .ofReal r ^ 2 * .ofReal π := by
  norm_num [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) x]

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