aemeasurable_fun_prod — Mathlib

English

Let s be a finite set and f_i: α → M. If each f_i is AEMeasurable, then the function a ↦ ∏_{i∈s} f_i(a) is AEMeasurable.

Русский

Пусть s — конечное множество и f_i: α → M. Если каждый f_i является AEMeasurable, то функция a ↦ ∏_{i∈s} f_i(a) измерима почти всюду.

LaTeX

$$$\forall s : \mathrm{Finset}\,\iota,\ (\forall i \in s,\ \mathrm{AEMeasurable}(f i) ) \rightarrow \mathrm{AEMeasurable}\bigl(\prod_{i \in s} f i\bigr).$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem aemeasurable_fun_prod (s : Finset ι) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) :
    AEMeasurable (fun a => ∏ i ∈ s, f i a) μ := by simpa only [← Finset.prod_apply] using s.aemeasurable_prod hf

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