volume_pi_closedBall — Mathlib

English

Volume of a closed ball in the product space equals the product of volumes of the component closed balls.

Русский

Объем замкнутого шара в произведении равен произведению объемов компонент замкнутых шаров.

LaTeX

$$$volume(\text{Metric.closedBall}(x,r)) = \prod_i volume(\text{Metric.closedBall}(x_i,r))$$$

Lean4

theorem volume_pi_closedBall [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))]
    [∀ i, MetricSpace (α i)] (x : ∀ i, α i) {r : ℝ} (hr : 0 ≤ r) :
    volume (Metric.closedBall x r) = ∏ i, volume (Metric.closedBall (x i) r) :=
  Measure.pi_closedBall _ _ hr

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