toMeasurableMul — Mathlib

English

If α carries a discrete measurable structure, then the multiplication map α × α → α is measurable. In particular, left and right multiplications by a fixed element are measurable.

Русский

Если у пространства α дискретная сигма-алгебра, то операция умножения α × α → α измерима; частный случай — левое и правое умножение на фиксированное элементы измеримы.

LaTeX

$$$\text{MeasurableMul}\,\alpha$, i.e. the map $(x,y) \mapsto x \cdot y$ is measurable on $\alpha \times \alpha$.$$

Lean4

@[to_additive] -- See note [lower instance priority]

instance (priority := 100) toMeasurableMul [DiscreteMeasurableSpace α] : MeasurableMul α
    where
  measurable_const_mul _ := .of_discrete
  measurable_mul_const _ := .of_discrete

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