English
Let f_i: α → β → M be a family of functions and g: α → β be measurable. If each f_i is measurable (in the appropriate sense) and g is measurable, then the composite a ↦ (∏_{i∈s} f_i(a))(g(a)) is measurable.
Русский
Пусть f_i: α → β → M образуют семейство функций и g: α → β измерим. При условии, что каждый f_i измерим, и g измерим, отображение a ↦ (∏_{i∈s} f_i(a))(g(a)) измеримо.
LaTeX
$$$\forall s : \mathrm{Finset}\,\iota\;\forall f : \iota \to \alpha \to \beta \to M\;\forall g : \alpha \to \beta,\; (\forall i \in s,\ \mathrm{Measurable} (f i)) \rightarrow \mathrm{Measurable}\bigl(a \mapsto \bigl(\prod_{i \in s} f i(a)\bigr)(g(a))\bigr).$$$
Lean4
/-- Compositional version of `Finset.measurable_prod` for use by `fun_prop`. -/
@[to_additive (attr := measurability, fun_prop) /--
Compositional version of `Finset.measurable_sum` for use by `fun_prop`. -/
]
theorem measurable_prod_apply {f : ι → α → β → M} {g : α → β} {s : Finset ι} (hf : ∀ i ∈ s, Measurable ↿(f i))
(hg : Measurable g) : Measurable fun a ↦ (∏ i ∈ s, f i a) (g a) := by simp only [prod_apply];
fun_prop (discharger := assumption)
