instMeasurableMul — Mathlib

English

There is a canonical MeasurableMul structure on MulOpposite M, induced by measurable operations on M.

Русский

Существует каноническая структура MeasurableMul на MulOpposite M, порождённая измеримыми операциями на M.

LaTeX

$$$\\text{MeasurableMul }(MulOpposite\\,M)$$$

Lean4

@[to_additive]
instance instMeasurableMul {M : Type*} [Mul M] [MeasurableSpace M] [MeasurableMul M] : MeasurableMul Mᵐᵒᵖ :=
  ⟨fun _ => measurable_mul_op.comp (measurable_mul_unop.mul_const _), fun _ =>
    measurable_mul_op.comp (measurable_mul_unop.const_mul _)⟩

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