measurableMul — Mathlib

English

If γ carries a continuous multiplication, then left and right multiplication by a fixed element are measurable; equivalently, the multiplication map γ × γ → γ is measurable.

Русский

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

LaTeX

$$$\\mathrm{MeasurableMul}(\\gamma) \\quad\\text{where }\\mu:(x,y)\\mapsto x\\cdot y\\text{ is measurable.}$$$

Lean4

@[to_additive]
instance (priority := 100) measurableMul [Mul γ] [ContinuousMul γ] : MeasurableMul γ
    where
  measurable_const_mul _ := (continuous_const.mul continuous_id).measurable
  measurable_mul_const _ := (continuous_id.mul continuous_const).measurable

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