instMeasurableConstSMul — Mathlib

English

If each component α_i has a MeasurableConstSMul by M, then the space of functions ∀ i, α_i has a MeasurableConstSMul by M.

Русский

Если каждый компонент пространства α_i имеет измеримое константное умножение M, то функциональное пространство ∀ i, α_i имеет такое же свойство.

LaTeX

$$$\text{MeasurableConstSMul } M (\prod_i α_i)$$$

Lean4

@[to_additive]
instance instMeasurableConstSMul {ι : Type*} {α : ι → Type*} [∀ i, SMul M (α i)] [∀ i, MeasurableSpace (α i)]
    [∀ i, MeasurableConstSMul M (α i)] : MeasurableConstSMul M (∀ i, α i) where
  measurable_const_smul _ := measurable_pi_iff.2 fun i ↦ (measurable_pi_apply i).const_smul _

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