volume_closedBall_fin_two

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

URI: https://scilib.ai/kg/mathlib#EuclideanSpace.volume_closedBall_fin_two

← MathLib Explorer

English

In E = R^2, the volume of the closed ball of radius r is π r^2.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem volume_closedBall_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ 2 * .ofReal π := by
  rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_two x r]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru