toMeasurableMul — Mathlib

English

There is a canonical way to make multiplication measurable on M by defining left and right translations as measurable maps.

Русский

Существует канонический способ придать измеримость умножению на M через левое и правое перенесение как измеримые отображения.

LaTeX

$$$\\text{MeasurableMul}(M)\\; \\text{exists with left and right translations measurable, i.e. } x \\mapsto a \\cdot x \\text{ and } x \\mapsto x \\cdot a \\text{ are measurable for all } a \\in M.$$$

Lean4

@[to_additive]
instance (priority := 100) toMeasurableMul [MeasurableMul₂ M] : MeasurableMul M :=
  ⟨fun _ => measurable_const.mul measurable_id, fun _ => measurable_id.mul measurable_const⟩

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