pi_closedBall — Mathlib

English

If each α_i is a metric space, the product closed ball has measure equal to the product of the measures of the coordinate closed balls.

Русский

Если каждое α_i — метрическое пространство, мера произведения замкнутого шара равна произведению мер соответствующих замкнутых шаров.

LaTeX

$$$(\pi\mu)(\mathrm{closedBall}(x,r)) = \prod_i \mu_i(\mathrm{closedBall}(x_i,r))$$$

Lean4

theorem pi_closedBall [∀ i, MetricSpace (α i)] (x : ∀ i, α i) {r : ℝ} (hr : 0 ≤ r) :
    Measure.pi μ (Metric.closedBall x r) = ∏ i, μ i (Metric.closedBall (x i) r) := by rw [closedBall_pi _ hr, pi_pi]

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