coe_comp_expOrderIso

Mathlib.Analysis.SpecialFunctions.Exp

URI: https://scilib.ai/kg/mathlib#Real.coe_comp_expOrderIso

English

Composing the inclusion with the order isomorphism yields the exponential function.

Русский

Сomposing with expOrderIso даёт экспоненту.

LaTeX

$$$\\mathrm{incl} \\circ \\mathrm{expOrderIso} = \\exp.$$$

Lean4

@[simp]
theorem coe_comp_expOrderIso : (↑) ∘ expOrderIso = exp :=
  rfl

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

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

Разделы

Аффилиация

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