comp_snd — Mathlib

English

If f : α × β → γ is measurable and for almost every y the map x ↦ f(x,y) is quasi-measure-preserving, then f is quasi-measure-preserving on μ×ν.

Русский

Если f измеримо и для почти всех y отображение x↦f(x,y) сохраняет меру, то f сохраняет меру на μ×ν.

LaTeX

$$QuasiMeasurePreserving f (μ × ν) τ$$

Lean4

theorem comp_snd {f : β → γ} (hf : NullMeasurable f ν) : NullMeasurable (fun z : α × β => f z.2) (μ.prod ν) :=
  hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd

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