comp_fst — Mathlib

English

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

Русский

Если f—NullMeasurable α→γ по μ, то (x,y)↦f(x) является NullMeasurable по μ×ν.

LaTeX

$$NullMeasurable f μ → NullMeasurable (fun z : α × β => f z.1) (μ × ν)$$

Lean4

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

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