prodMk — Mathlib

English

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

Русский

Если f и g являются AEStronglyMeasurable относительно μ, тогда функция x ↦ (f(x), g(x)) является AEStronglyMeasurable относительно μ.

LaTeX

$$$AEStronglyMeasurable\, f\, μ \;\\rightarrow\\; AEStronglyMeasurable\, g\, μ \;\\rightarrow\\; AEStronglyMeasurable\\left( x \\mapsto (f(x),\\, g(x))\\right)\\, μ$$$

Lean4

@[fun_prop]
protected theorem prodMk {f : α → β} {g : α → γ} (hf : AEStronglyMeasurable[m] f μ) (hg : AEStronglyMeasurable[m] g μ) :
    AEStronglyMeasurable[m] (fun x => (f x, g x)) μ :=
  ⟨fun x => (hf.mk f x, hg.mk g x), hf.stronglyMeasurable_mk.prodMk hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩

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