pow — Mathlib

English

If f and g are almost everywhere measurable, then x ↦ f(x)^g(x) is almost everywhere measurable.

Русский

Если f и g измеримы почти всюду, то x ↦ f(x)^g(x) измеримо почти всюду.

LaTeX

$$$\\text{AEMeasurable}(f) \\Rightarrow \\text{AEMeasurable}(g) \\Rightarrow \\text{AEMeasurable}(x \\mapsto f(x)^{\\,g(x)}).$$$

Lean4

@[aesop safe 20 apply (rule_sets := [Measurable]), fun_prop]
theorem pow (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun x => f x ^ g x) μ :=
  measurable_pow.comp_aemeasurable (hf.prodMk hg)

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