English
If g: β → β' → γ is such that its curried form is continuous, and f: α → β, f': α → β' are AEStronglyMeasurable, then the composition x ↦ g(f(x), f'(x)) is AEStronglyMeasurable.
Русский
Если g: β × β' → γ непрерывна в аргументах через раскручиваемую форму, и f: α → β, f': α → β' аэр AEStronglyMeasurable, то композиция x ↦ g(f(x), f'(x)) является AEStronglyMeasurable.
LaTeX
$$$AEStronglyMeasurable\ f\ μ \\rightarrow AEStronglyMeasurable\ f'\ μ \\rightarrow AEStronglyMeasurable\left( x \mapsto g\bigl(f(x), f'(x)\bigr)\right) μ$$$
Lean4
/-- The composition of a continuous function of two variables and two ae strongly measurable
functions is ae strongly measurable. -/
theorem _root_.Continuous.comp_aestronglyMeasurable₂ {β' : Type*} [TopologicalSpace β'] {g : β → β' → γ} {f : α → β}
{f' : α → β'} (hg : Continuous g.uncurry) (hf : AEStronglyMeasurable[m] f μ) (h'f : AEStronglyMeasurable[m] f' μ) :
AEStronglyMeasurable[m] (fun x => g (f x) (f' x)) μ :=
hg.comp_aestronglyMeasurable (hf.prodMk h'f)
