ereal_exp

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

← MathLib Explorer

English

For any measurable f, the map x ↦ exp(f(x)) is measurable.

Русский

Для измеримой функции f горизонтальная экспонента измерима.

LaTeX

$$$\text{Measurable}(x \mapsto \exp(f(x)))$$$

Lean4

@[measurability, fun_prop]
theorem _root_.Measurable.ereal_exp {α : Type*} {_ : MeasurableSpace α} {f : α → EReal} (hf : Measurable f) :
    Measurable fun x ↦ exp (f x) :=
  measurable_exp.comp hf

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

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

Разделы

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

Аффилиация

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