prodMk — Mathlib

English

If f and g are AEMeasurable with respect to μ, then the map x ↦ (f x, g x) is AEMeasurable with respect to μ.

Русский

Пусть f и g — AЕ-измеримые относительно μ; тогда x ↦ (f x, g x) — AЕ-измеримая относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow \mathrm{AEMeasurable}(g, \mu) \rightarrow \mathrm{AEMeasurable}(\lambda x. (f x, g x), \mu)$$$

Lean4

@[fun_prop, measurability]
theorem prodMk {f : α → β} {g : α → γ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun x => (f x, g x)) μ :=
  ⟨fun a => (hf.mk f a, hg.mk g a), hf.measurable_mk.prodMk hg.measurable_mk, hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩

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