pi_Iio_ae_eq_pi_Iic — Mathlib

English

The product of open intervals Iio(f_i) across I equals almost everywhere to the product of closed intervals Iic(f_i) for a given f, under a measure with sigma-finite components and no atoms assumptions as required.

Русский

Произведение открытых интервалов Iio(f_i) по I а.е. равно произведению замкнутых интервалов Iic(f_i) при заданной мере с сигма-скороимостью и отсутствием атомов.

LaTeX

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

Lean4

theorem pi_Iio_ae_eq_pi_Iic {s : Set ι} {f : ∀ i, α i} :
    (pi s fun i => Iio (f i)) =ᵐ[Measure.pi μ] pi s fun i => Iic (f i) :=
  ae_eq_set_pi fun _ _ => Iio_ae_eq_Iic

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