aestronglyMeasurable_prod — Mathlib

English

If finitely many functions f_i are AEStronglyMeasurable, then the product ∏ f_i is AEStronglyMeasurable.

Русский

Если конечное число функций f_i AEStronglyMeasurable, тогда произведение ∏ f_i 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_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (∏ i ∈ s, f i) μ :=
  Multiset.aestronglyMeasurable_prod _ fun _g hg =>
    let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg
    hg ▸ hf _ hi

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