exp_half

Mathlib.Analysis.SpecialFunctions.Exp

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

English

exp(x/2) = sqrt(exp x).

Русский

exp(x/2) = sqrt(exp x).

LaTeX

$$$$ \\exp\\left( \\frac{x}{2} \\right) = \\sqrt{\\exp x}. $$$$

Lean4

theorem exp_half (x : ℝ) : exp (x / 2) = √(exp x) := by
  rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves] <;> exact (exp_pos _).le

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

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

Разделы

Аффилиация

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