toMeasurableSMul — Mathlib

English

The scalar action by M on α is measurable, i.e., (m,a) ↦ m•a is measurable.

Русский

Действие скаляра M на α измеримо: (m,a) ↦ m•a измеримо.

LaTeX

$$$\\mathrm{MeasurableSMul}(M,\\alpha)\\;\\text{with }(m,a)\\mapsto m\\cdot a.$$$

Lean4

@[to_additive]
instance (priority := 100) toMeasurableSMul {M α} [TopologicalSpace M] [TopologicalSpace α] [MeasurableSpace M]
    [MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul M α
    where measurable_smul_const _ := (continuous_id.smul continuous_const).measurable

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