pi_pi — Mathlib

English

Let ι be finite and μ_i sigma-finite. For any cylinder s = (s_i) with s_i ⊆ α_i, the product measure of the cylinder equals the product of the individual measures.

Русский

Пусть ι конечен и μ_i сигма-конечны. Для цилиндра s = (s_i) с s_i ⊆ α_i мера произведения равна произведению мер μ_i(s_i).

LaTeX

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

Lean4

@[simp]
theorem pi_pi [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) : Measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
  by
  haveI : Encodable ι := Fintype.toEncodable ι
  rw [← pi'_eq_pi, pi'_pi]

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