pow_const

Mathlib.MeasureTheory.Group.Arithmetic

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

English

If g is measurable, then the map x ↦ c^{g(x)} is measurable for fixed c.

Русский

Если g измеримо, то x ↦ c^{g(x)} измеримо для фиксированного c.

LaTeX

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

Lean4

@[fun_prop, measurability]
theorem pow_const (hf : Measurable f) (c : γ) : Measurable fun x => f x ^ c :=
  hf.pow measurable_const

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

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

Разделы

Аффилиация

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