aestronglyMeasurable_fun_prod — Mathlib

English

If f maps α to β and is AEStronglyMeasurable for each f in a finite set, then the map x ↦ ∏ f_i(x) is AEStronglyMeasurable.

Русский

Если даны функции из множества и каждая из них AEStronglyMeasurable, то произведение по i ∈ S f_i(x) AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\\ f\, μ \\rightarrow AEStronglyMeasurable\\ g\, μ \\Rightarrow AEStronglyMeasurable\\left(x \\mapsto f(x) \\cdot g(x)\\right) μ$$$

Lean4

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

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