instMeasurableSMul — Mathlib

English

Restriction of a measurable SMul on M to a Submonoid s yields a measurable SMul on s acting on α; i.e., the induced action of s on α is measurable.

Русский

Ограничение измеримого действия SMul на M до подмоноида s даёт измеримое действие на α.

LaTeX

$$$\text{MeasurableSMul}(\text{Subtype } p:(p.1\in s),\alpha)$$$

Lean4

@[to_additive]
instance instMeasurableSMul {M α} [MeasurableSpace M] [MeasurableSpace α] [Monoid M] [MulAction M α]
    [MeasurableSMul M α] (s : Submonoid M) : MeasurableSMul s α where
  measurable_smul_const x := (measurable_smul_const (M := M) x).comp measurable_subtype_coe

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