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]