map_prod_map — Mathlib

English

If f and g are measurable, then mapping after product equals mapping of the product after mapping: (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g).

Русский

Если функции f и g измеримы, то отображение после произведения равно отображению произведения после отображения: (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g).

LaTeX

$$$ (\mu.map f) \mathrm{prod} (\nu.map g) = (\mu \mathrm{prod} \nu).\mathrm{map} (\mathrm{Prod.map} f g) $$$

Lean4

theorem map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β'] {f : α → α'} {g : β → β'}
    (f_mble : Measurable f) (g_mble : Measurable g) : (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g) :=
  by
  apply Subtype.ext
  simp only [val_eq_toMeasure, toMeasure_prod, toMeasure_map]
  rw [Measure.map_prod_map _ _ f_mble g_mble]

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