measurableSMul₂_of_mul — Mathlib

English

If M has a measurable multiplication and a MeasurableMul₂ structure (two-variable measurability of multiplication), then the two-variable smul of M on M is measurable; i.e., the map (a,b) ↦ a b is measurable when viewed as a function of two variables.

Русский

Пусть M имеет измеримое умножение и структуру MeasurableMul₂; тогда двуарная операция умножения на M есть измерима функция (a,b) ↦ a b.

LaTeX

$$$\mathrm{MeasurableSMul_2}\; M\; M\,=\;\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 :=
  ⟨measurable_mul⟩

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