exp

Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

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

English

If f: Ω → ℝ is measurable, then x ↦ exp(f(x)) is measurable.

Русский

Если f: Ω → ℝ измерима, то x ↦ e^{f(x)} измерима.

LaTeX

$$$\\\\operatorname{Measurable}(f) \\\\Rightarrow \\\\operatorname{Measurable}(\\\\lambda x. \\\\exp(f(x)))$$$

Lean4

@[measurability, fun_prop]
protected theorem exp : Measurable fun x => Real.exp (f x) :=
  Real.measurable_exp.comp hf

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

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

Разделы

Аффилиация

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