differentiableAt_log

Mathlib.Analysis.SpecialFunctions.Log.Deriv

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

English

Let x be a real number with x ≠ 0. Then the natural logarithm is differentiable at x.

Русский

Пусть x ∈ ℝ и x ≠ 0. Тогда логарифм по основанию e дифференцируем в точке x.

LaTeX

$$$x \neq 0 \\Rightarrow \\mathrm{DifferentiableAt}_{\\mathbb{R}}(\\log, x)$$$

Lean4

@[fun_prop]
theorem differentiableAt_log (hx : x ≠ 0) : DifferentiableAt ℝ log x :=
  (hasDerivAt_log hx).differentiableAt

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

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

Разделы

Аффилиация

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