prod_swap — Mathlib

English

If f: β×α → γ is AEMeasurable with respect to ν×μ, then f( z.swap ) is AEMeasurable with respect to μ×ν.

Русский

Если f : β×α → γ измеримо почти всюду относительно ν×μ, то f(z.swap) измеримо почти всюду относительно μ×ν.

LaTeX

$$AEMeasurable f (ν × μ) → AEMeasurable (fun z => f z.swap) (μ × ν)$$

Lean4

theorem prod_swap [SFinite μ] [SFinite ν] {f : β × α → γ} (hf : AEMeasurable f (ν.prod μ)) :
    AEMeasurable (fun z : α × β => f z.swap) (μ.prod ν) :=
  by
  rw [← Measure.prod_swap] at hf
  exact hf.comp_measurable measurable_swap

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