English
For families of spaces (α i) with measurable multiplications, the pointwise product on the function space ∀ i, α i is measurable coordinatewise.
Русский
Для семейств пространств с помножением по точке в пространстве функций ∀ i, α_i измеримость координатной суммы сохраняется.
LaTeX
$$$[\\forall i, \\text{MeasurableMul}(\\alpha_i)] \\Rightarrow \\text{MeasurableMul}(\\,\\forall i, \\alpha_i\\,).$$$
Lean4
@[to_additive]
instance measurableMul {ι : Type*} {α : ι → Type*} [∀ i, Mul (α i)] [∀ i, MeasurableSpace (α i)]
[∀ i, MeasurableMul (α i)] : MeasurableMul (∀ i, α i) :=
⟨fun _ => measurable_pi_iff.mpr fun i => (measurable_pi_apply i).const_mul _, fun _ =>
measurable_pi_iff.mpr fun i => (measurable_pi_apply i).mul_const _⟩
