univ_pi_Ioo_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) равно практически повсеместно Icc(f_i).

LaTeX

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

Lean4

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

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