log_of_ne_zero

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

For x ≠ 0, log x equals the inverse of the exponential on |x|; equivalently, log x = ln|x|.

Русский

Пусть x ≠ 0. Тогда log x равен обратной экспоненте на множество {|x|}; эквивалентно log x = ln|x|.

LaTeX

$$$x \neq 0 \Rightarrow \log x = \ln|x|$$$

Lean4

theorem log_of_ne_zero (hx : x ≠ 0) : log x = expOrderIso.symm ⟨|x|, abs_pos.2 hx⟩ :=
  dif_neg hx

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

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

Разделы

Аффилиация

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