expOrderIso

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

URI: https://scilib.ai/kg/mathlib#EReal.expOrderIso

← MathLib Explorer

English

log(x^y) = y log x for x>0, extended to ENNReal with proper conventions.

Русский

log(x^y) = y log x при x>0, обобщение на ENNReal с учётом условий.

LaTeX

$$$\\log(x^y) = y \\cdot \\log x$$$

Lean4

/-- `EReal.exp` and its inverse `ENNReal.log` are an order isomorphism between `EReal` and
`ℝ≥0∞`. -/
noncomputable def _root_.EReal.expOrderIso :=
  logOrderIso.symm

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

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

Разделы

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

Аффилиация

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