continuous_log

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

English

The logarithm on ENNReal is a continuous map: log: ENNReal → EReal is continuous.

Русский

Логарифм на ENNReal непрерывен: log: ENNReal → EReal непрерывен.

LaTeX

$$$$\log \in C\bigl(\mathrm{ENNReal}, \mathrm{EReal}\bigr)$$$$

Lean4

@[continuity, fun_prop]
theorem continuous_log : Continuous log :=
  logOrderIso.continuous

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

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

Разделы

Аффилиация

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