univ_pi_Ico_ae_eq_Icc — Mathlib

English

The universal product of Ioo(f_i) is a.e. equal to the universal product of Icc(f_i).

Русский

Универсальное произведение Ioo(f_i) равно a.e. произведению Icc(f_i).

LaTeX

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

Lean4

theorem univ_pi_Ico_ae_eq_Icc {f g : ∀ i, α i} : (pi univ fun i => Ico (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g := by
  rw [← pi_univ_Icc]; exact pi_Ico_ae_eq_pi_Icc

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