expHomeomorph

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

English

The order isomorphism logOrderIso is continuous in both directions.

Русский

Порядковая изоморфия logOrderIso непрерывна в обе стороны.

LaTeX

$$Continuous (logOrderIso)$$

Lean4

/-- `exp` as a homeomorphism. -/
noncomputable def _root_.EReal.expHomeomorph : EReal ≃ₜ ℝ≥0∞ :=
  expOrderIso.toHomeomorph

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

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

Разделы

Аффилиация

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