differentiableOn_log

Mathlib.Analysis.SpecialFunctions.Log.Deriv

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

English

The logarithm is differentiable at every point of the real line except 0; i.e., on ℝ \ {0}.

Русский

Логарифм дифференцируем на всей числовой прямой, за исключением нуля; т.е. на ℝ \ {0}.

LaTeX

$$DifferentiableOn ℝ log (Set.compl {0})$$

Lean4

theorem differentiableOn_log : DifferentiableOn ℝ log {0}ᶜ := fun _x hx =>
  (differentiableAt_log hx).differentiableWithinAt

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

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

Разделы

Аффилиация

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