volume_ball — Mathlib

English

Let a ∈ ℝ and r ∈ ℝ. The volume of the ball of radius r around a is equal to the length 2r, encoded as the appropriate nonnegative extended real.

Русский

Пусть a ∈ ℝ и r ∈ ℝ. Объем шара радиуса r с центром a равен длине 2r (в соответствующем н-мерном контексте), т.е. объём равен 2r.

LaTeX

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

Lean4

@[simp]
theorem volume_ball (a r : ℝ) : volume (Metric.ball a r) = ofReal (2 * r) := by
  rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]

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