aestronglyMeasurable_fun_prod — Mathlib

English

If finitely many functions f_i are AEStronglyMeasurable, then the map a ↦ ∏ i∈S f_i(a) is AEStronglyMeasurable.

Русский

Если конечное число функций f_i AEStronglyMeasurable, тогда функция a ↦ ∏ i∈S f_i(a) AEStronglyMeasurable.

LaTeX

$$$\forall i \in S, AEStronglyMeasurable\ f_i μ \rightarrow AEStronglyMeasurable\left(\prod i \in S, f_i\right) μ$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem _root_.Finset.aestronglyMeasurable_fun_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ := by
  simpa only [← Finset.prod_apply] using s.aestronglyMeasurable_prod hf

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