toMeasurableConstSMul — Mathlib

English

If a type α has a scalar action by M with ContinuousConstSMul, then constant scalar multiplication maps are measurable.

Русский

Если задано действие скаляра на α и есть непрерывное константное умножение, то отображения константного умножения измеримы.

LaTeX

$$$\\forall c:\\\,M,\\text{Measurable}(\\lambda a:\\,\\alpha, c\\cdot a).$$$

Lean4

@[to_additive]
instance (priority := 100) toMeasurableConstSMul {M α} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
    [SMul M α] [ContinuousConstSMul M α] : MeasurableConstSMul M α where
  measurable_const_smul _ := (continuous_const_smul _).measurable

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