measurableMul₂ — Mathlib

English

There is a canonical MeasurableMul₂ structure on the Pi-type (ι → α_i), given coordinatewise by measurability of projections and multiplication.

Русский

Существует каноническая структура MeasurableMul₂ на типе Πι α_i, заданная по координатам через измеримость проекций и умножения.

LaTeX

$$$\\text{MeasurableMul}_2((f,g))\\;\\text{ для } f,g: (i \\to \\alpha_i).$$$

Lean4

@[to_additive Pi.measurableAdd₂]
instance measurableMul₂ {ι : Type*} {α : ι → Type*} [∀ i, Mul (α i)] [∀ i, MeasurableSpace (α i)]
    [∀ i, MeasurableMul₂ (α i)] : MeasurableMul₂ (∀ i, α i) :=
  ⟨measurable_pi_iff.mpr fun _ => measurable_fst.eval.mul measurable_snd.eval⟩

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