log_of_pos

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

If x > 0, then log x equals the ordinary natural logarithm of x; i.e., log x = ln x.

Русский

Пусть x > 0. Тогда log x = ln x.

LaTeX

$$$x > 0 \Rightarrow \log x = \ln x$$$

Lean4

theorem log_of_pos (hx : 0 < x) : log x = expOrderIso.symm ⟨x, hx⟩ :=
  by
  rw [log_of_ne_zero hx.ne']
  congr
  exact abs_of_pos hx

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

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

Разделы

Аффилиация

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