cosh_log

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

For x > 0, cosh(log x) = (x + x^{-1})/2.

Русский

Для x > 0: cosh(log x) = (x + x^{-1})/2.

LaTeX

$$$x > 0 \Rightarrow \cosh(\log x) = \dfrac{x + x^{-1}}{2}$$$

Lean4

theorem cosh_log {x : ℝ} (hx : 0 < x) : cosh (log x) = (x + x⁻¹) / 2 := by rw [cosh_eq, exp_neg, exp_log hx]

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

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

Разделы

Аффилиация

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