univ_pi_Ioi_ae_eq_Ici — Mathlib

English

For the full product, the a.e. equality between the product of Ioi(f_i) and Ici(f_i) holds under the product measure.

Русский

Для полного произведения выполняется ae-равенство продукции Ioi(f_i) и Ici(f_i).

LaTeX

$$$(\\mathrm{pi}\\; \\mathrm{univ}\\; (\\lambda i.\\; \\mathrm{Ioi}(f_i))) =_{a.e.}^{\\mathrm{Measure.pi}\\; \\mu} \\mathrm{Ici}(f)$$$

Lean4

theorem univ_pi_Ioi_ae_eq_Ici {f : ∀ i, α i} : (pi univ fun i => Ioi (f i)) =ᵐ[Measure.pi μ] Ici f := by
  rw [← pi_univ_Ici]; exact pi_Ioi_ae_eq_pi_Ici

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