instMeasurableConstSMul — Mathlib

English

If M is a monoid and β carries a measurable action of M, then the action of units of M (i.e., Mˣ) on β is measurable with respect to the SMul structure. Consequently, the units inherit a compatible MeasurableSMul structure on β.

Русский

Пусть M — моноид, β — множество с измеримым действием от M. Тогда гамма-единиц Mˣ действует на β измеримо, и структура MeasurableSMul переходит на Units M.

LaTeX

$$$MeasurableSMul (Units\,M)\,\\beta$$$

Lean4

@[to_additive]
instance instMeasurableConstSMul : MeasurableConstSMul Mˣ β where
  measurable_const_smul c := measurable_const_smul (c : M)

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