comp_snd — Mathlib

English

If f is quasi-measure-preserving on a product, then both its first and second coordinate projections are quasi-measure-preserving.

Русский

Если отображение сохраняет меру на произведение, то проекции на первую и вторую координату сохраняют меру.

LaTeX

$$QuasiMeasurePreserving (fun x => (f x).1) μ ν ∧ QuasiMeasurePreserving (fun x => (f x).2) μ τ$$

Lean4

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

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