pi_Ioo_ae_eq_pi_Icc — Mathlib

English

The product of Ioo(f_i) across i is almost everywhere equal to the product of Icc(f_i) across i, under the product measure.

Русский

Производное произведение Ioo(f_i) по i почти равно произведению Icc(f_i) по i по мере произведения.

LaTeX

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

Lean4

theorem pi_Ioo_ae_eq_pi_Icc {s : Set ι} {f g : ∀ i, α i} :
    (pi s fun i => Ioo (f i) (g i)) =ᵐ[Measure.pi μ] pi s fun i => Icc (f i) (g i) :=
  ae_eq_set_pi fun _ _ => Ioo_ae_eq_Icc

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