univ_pi_Iio_ae_eq_Iic — Mathlib

English

When taking the product over all indices with Iio(f_i), the almost-everywhere equality to the product over Iic(f_i) holds for the universal indexing set.

Русский

При полном произведении по всем индексам интервал Iio(f_i) почти равно Iic(f_i) по a.e. на всем индексе.

LaTeX

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

Lean4

theorem univ_pi_Iio_ae_eq_Iic {f : ∀ i, α i} : (pi univ fun i => Iio (f i)) =ᵐ[Measure.pi μ] Iic f := by
  rw [← pi_univ_Iic]; exact pi_Iio_ae_eq_pi_Iic

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