English
Let s be a finite subset of ι and suppose each f_i is almost everywhere measurable with respect to μ. Then the product ∏_{i∈s} f_i is almost everywhere measurable with respect to μ.
Русский
Пусть s — конечное подмножество ι, и пусть каждый f_i измерим почти всюду относительно меры μ. Тогда произведение ∏_{i∈s} f_i измеримо почти всюду относительно μ.
LaTeX
$$$\forall s : \mathrm{Finset}\,\iota,\; (\forall i \in s,\ \mathrm{AEMeasurable}(f i)\, \mu)\rightarrow \mathrm{AEMeasurable}\bigl(\prod_{i \in s} f i\bigr)\mu$$$
Lean4
@[to_additive (attr := measurability, fun_prop)]
theorem aemeasurable_prod (s : Finset ι) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (∏ i ∈ s, f i) μ :=
Multiset.aemeasurable_prod _ fun _g hg =>
let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg
hg ▸ hf _ hi
