comp_fst — Mathlib

English

If f is AEMeasurable from α to γ, then (x,y) ↦ f(x) is AEMeasurable with respect to μ×ν.

Русский

Если f измеримо почти всюду с α→γ, то (x,y)↦f(x) измеримо почти всюду по μ×ν.

LaTeX

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

Lean4

theorem comp_fst {f : α → γ} (hf : AEMeasurable f μ) : AEMeasurable (fun z : α × β => f z.1) (μ.prod ν) :=
  hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst

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