pi_ball — Mathlib

English

If each α_i is a metric space, the measure of a product ball equals the product of the measures of the corresponding balls.

Русский

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

LaTeX

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

Lean4

theorem pi_ball [∀ i, MetricSpace (α i)] (x : ∀ i, α i) {r : ℝ} (hr : 0 < r) :
    Measure.pi μ (Metric.ball x r) = ∏ i, μ i (Metric.ball (x i) r) := by rw [ball_pi _ hr, pi_pi]

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