English
Let (f_i)_{i∈ι} be a family of measurable functions f_i: α → M, where M is a measurable space and α is equipped with a measurable space. For any finite set s ⊂ ι, the function a ↦ ∏_{i∈s} f_i(a) is measurable.
Русский
Пусть (f_i)_{i∈ι} — семейство измеримых функций f_i: A → M, где M — пространство с измеримостью, A — множество с измеримостью. Для любого конечного подмножества s ⊂ ι функция a ↦ ∏_{i∈s} f_i(a) измерима.
LaTeX
$$$\forall s : \mathrm{Finset}\,\iota,\; (\forall i \in s,\ \mathrm{Measurable}(f\,i)) \rightarrow \mathrm{Measurable}\bigl(a \mapsto \prod_{i \in s} f_i(a)\bigr) $$$
Lean4
@[to_additive (attr := measurability, fun_prop)]
theorem measurable_prod (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun a ↦ ∏ i ∈ s, f i a :=
by
simp_rw [← Finset.prod_apply]
exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf
