pi_Ioc_ae_eq_pi_Icc — Mathlib

English

The a.e. equality for Ioc to Icc transfers to the product over I.

Русский

Ae-равенство для Ioc к Icc переносится в произведение по I.

LaTeX

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

Lean4

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

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