aemeasurable2 — Mathlib

English

If h is continuous on α×β and f,g are AEMeasurable, then a ↦ h(f(a), g(a)) is AEMeasurable.

Русский

Если h непрерывна на α×β, а f,g — а.е.-измеримы, то a↦h(f(a),g(a)) а.е.-измерима.

LaTeX

$$$\\text{Continuous}(p\\mapsto c(p.fst,p.snd))\\land\\mathrm{AEMeasurable}(f)\\land\\mathrm{AEMeasurable}(g)\\Rightarrow\\mathrm{AEMeasurable}(a\\mapsto c(f(a),g(a))).$$$

Lean4

theorem aemeasurable2 [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : Measure δ}
    (h : Continuous fun p : α × β => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun a => c (f a) (g a)) μ :=
  h.measurable.comp_aemeasurable (hf.prodMk hg)

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