English
Let M be a type with a measurable space structure and a measurable multiplication. Then the left action of M on itself by multiplication is measurable; equivalently, the map (a,b) ↦ a b is measurable, and for each fixed a the map b ↦ a b is measurable, and for each fixed b the map a ↦ a b is measurable.
Русский
Пусть имеется множество M с измеримым пространством и измеримой операцией умножения. Тогда левого действия M на себя по умножению измеримо; то есть отображение (a,b) ↦ a b из M × M в M измеримо, а также для фиксированного a функция b ↦ a b и для фиксированного b функция a ↦ a b измеримы.
LaTeX
$$$\mathrm{Measurable}(\lambda p:(M\times M), p.1\cdot p.2)$$$
Lean4
@[to_additive]
instance measurableSMul_of_mul (M : Type*) [Mul M] [MeasurableSpace M] [MeasurableMul M] : MeasurableSMul M M
where
measurable_const_smul := measurable_id.const_mul
measurable_smul_const := measurable_id.mul_const
