deriv_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

URI: https://scilib.ai/kg/mathlib#deriv_arctan

← MathLib Explorer

English

For differentiable f, the derivative of arctan(f(x)) is (1/(1+f(x)^2))·f'(x).

Русский

Для дифференцируемой f производная arctan(f(x)) равна (1/(1+f(x)^2))·f'(x).

LaTeX

$$$ \text{deriv_arctan }(f) = \frac{1}{1+f(x)^2} \cdot f'(x). $$$

Lean4

@[simp]
theorem deriv_arctan (hc : DifferentiableAt ℝ f x) : deriv (fun x => arctan (f x)) x = 1 / (1 + f x ^ 2) * deriv f x :=
  hc.hasDerivAt.arctan.deriv

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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