measurable_fun_prod — Mathlib

English

If a finite set of functions are measurable, then the function a ↦ ∏ i∈s f_i(a) is measurable.

Русский

Если конечное множество функций измеримо, то отображение a ↦ ∏ i∈s f_i(a) измеримо.

LaTeX

$$$\\text{Measurable } a \\mapsto \\prod_{i\\in s} f_i(a)$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem measurable_fun_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

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