pow

Mathlib.MeasureTheory.Group.Arithmetic

URI: https://scilib.ai/kg/mathlib#Measurable.pow

← MathLib Explorer

English

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

Русский

Если f и g измеримы, то x ↦ f(x)^g(x) измеримо.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru