measurable_log

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

URI: https://scilib.ai/kg/mathlib#ENNReal.measurable_log

English

The logarithm function on ENNReal is measurable.

Русский

Логарифм на ENNReal измерим.

LaTeX

$$$\text{log}: \mathbb{R}_{\ge 0}^{\infty} \to \mathbb{E}$ является измеримой$$

Lean4

@[measurability, fun_prop]
theorem measurable_log : Measurable log :=
  continuous_log.measurable

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

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

Разделы

Аффилиация

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