instMeasurableConstSMul — Mathlib

English

If S is a submonoid of a monoid M acting on α with a measurable-constant-smul structure, then the restricted action of S on α is measurable.

Русский

Если S является подМОноида M и действует на α с измеримым действием умножения константой, то ограниченное действие S на α измеримо.

LaTeX

$$$\forall s \in S,\ \text{Measurable}(x \mapsto s\cdot x)$$$

Lean4

@[to_additive]
instance instMeasurableConstSMul {M α} [MeasurableSpace α] [Monoid M] [MulAction M α] [MeasurableConstSMul M α]
    (s : Submonoid M) : MeasurableConstSMul s α where
  measurable_const_smul c := by simpa only using measurable_const_smul (c : M)

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