const_pow — Mathlib

English

If g is measurable, then x ↦ c^{g(x)} is measurable (constant base, variable exponent).

Русский

Если g измеримо, то x ↦ c^{g(x)} измеримо (основание константа, показатель переменный).

LaTeX

$$$\\text{Measurable}(g) \\Rightarrow \\text{Measurable}(x \\mapsto c^{\,g(x)}).$$$

Lean4

@[fun_prop, measurability]
theorem const_pow (hg : Measurable g) (c : β) : Measurable fun x => c ^ g x :=
  measurable_const.pow hg

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