toMeasurableMul₂ — Mathlib

English

In a discrete measurable space, the two-variable multiplication is measurable, yielding a MeasurableMul₂ structure.

Русский

В дискретном измеримом пространстве операция умножения двух аргументов измерима, образуя структуру MeasurableMul₂.

LaTeX

$$$\text{MeasurableMul₂}\,\alpha$$$

Lean4

@[to_additive DiscreteMeasurableSpace.toMeasurableAdd₂] -- See note [lower instance priority]

instance (priority := 100) toMeasurableMul₂ [DiscreteMeasurableSpace (α × α)] : MeasurableMul₂ α :=
  ⟨.of_discrete⟩

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