English
Let I be a subset of indices and s, t be families of subsets. If for every i in I, the sets s_i and t_i are equal almost everywhere with respect to μ_i, then the indexed product sets π_I s and π_I t are equal almost everywhere with respect to the product measure Measure.pi μ.
Русский
Пусть I — подмножество индексов, а s, t — семейства подмножеств. Если для каждого i ∈ I множества s_i и t_i совпадают почти повсюду по μ_i, то соответствующие произведения π_I s и π_I t совпадают почти повсюду по Measure.pi μ.
LaTeX
$$$\\bigl( \\forall i \\in I,\; s_i =_{\\mu_i}^{\\mathrm{ae}} t_i \\bigr) \\Rightarrow (\\mathrm{Set.pi}\\; I\\; s =_{\\mathrm{ae}}^{\\mathrm{Measure.pi}\\; \\mu} \\mathrm{Set.pi}\\; I\\; t)$$$
Lean4
theorem ae_eq_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s i =ᵐ[μ i] t i) :
Set.pi I s =ᵐ[Measure.pi μ] Set.pi I t :=
(ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le)
