measurable2 — Mathlib

English

If f: δ → α and g: δ → β are measurable, and h: α × β → γ is continuous, then a(a) := h(f(a), g(a)) is measurable (under second countable assumptions).

Русский

Если f: δ→α и g: δ→β измеримы, а h: α×β→γ непрерывна, то a↦h(f(a), g(a)) измеримо (при требуемых предположениях о счётом размере).

LaTeX

$$$\\text{Continuous}(h)\\land\\mathrm{Measurable}(f)\\land\\mathrm{Measurable}(g)\\Rightarrow\\mathrm{Measurable}(a\\mapsto h(f(a),g(a))).$$$

Lean4

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

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