measurable_fun_prod — Mathlib

English

For a multiset of functions s, if each f is measurable, then the function a ↦ (∑ over s of f) a (interpreted via product) is measurable.

Русский

Для мультисета функций s, если каждая функция измерима, то соответствующее произведение функций является измеримым.

LaTeX

$$$\\text{Measurable }\\bigl( a \\mapsto (\\text{map}(f \\mapsto f(a), s)).prod \\bigr)$$$

Lean4

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

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