pi_univ — Mathlib

English

For finite ι and sigma-finite μ_i, the product measure on the full product space satisfies (π μ)(univ) = ∏ μ_i(univ).

Русский

Для конечного множества индексов ι и сигма-конечных мер μ_i мера произведения на полном пространстве равна произведению масс μ_i на всём пространстве.

LaTeX

$$$(\pi\mu)(\mathrm{univ}) = \prod_i \mu_i(\mathrm{univ})$$$

Lean4

nonrec theorem pi_univ [∀ i, SigmaFinite (μ i)] : Measure.pi μ univ = ∏ i, μ i univ := by rw [← pi_univ, pi_pi μ]

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