measurableSMul — Mathlib

English

If each coordinate α_i has a MeasurableConstSMul by M, then the function space ∀ i, α_i has a MeasurableConstSMul by M.

Русский

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

LaTeX

$$$\text{MeasurableConstSMul } M ((i: I) \to α_i)$$$

Lean4

@[to_additive]
instance measurableSMul {ι : Type*} {α : ι → Type*} [∀ i, SMul M (α i)] [∀ i, MeasurableSpace (α i)]
    [∀ i, MeasurableSMul M (α i)] : MeasurableSMul M (∀ i, α i) where
  measurable_smul_const _ := measurable_pi_iff.2 fun _ ↦ measurable_smul_const _

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