exp_eq_exp_ℝ

Mathlib.Analysis.SpecialFunctions.Exponential

URI: https://scilib.ai/kg/mathlib#Real.exp_eq_exp_ℝ

English

On the real numbers, Real.exp equals the standard exponential map coming from NormedSpace.exp on ℝ.

Русский

На множестве действительных чисел Real.exp совпадает с обычной экспонентой.

LaTeX

$$$$ \text{Real.exp} = \text{NormedSpace.exp } \mathbb{R}. $$$$

Lean4

theorem exp_eq_exp_ℝ : Real.exp = NormedSpace.exp ℝ := by ext x; exact mod_cast congr_fun Complex.exp_eq_exp_ℂ x

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

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

Разделы

Аффилиация

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