measurable_fun_prod — Mathlib

English

If l is a list of functions with measurable elements, then the function a ↦ ∏ i ∈ l, f i a is measurable.

Русский

Если в списке функций все функции измеримы, то отображение a ↦ произведение по i из списка f i a измеримо.

LaTeX

$$$\\text{Measurable } (\\lambda a. \\prod_{i} f_i(a))$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem measurable_fun_prod (l : List (α → M)) (hl : ∀ f ∈ l, Measurable f) :
    Measurable fun x => (l.map fun f : α → M => f x).prod := by
  simpa only [← Pi.list_prod_apply] using l.measurable_prod hl

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