deriv_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

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

English

The derivative of arctan at x equals 1/(1+x^2) for differentiable points.

Русский

Производная arctan в точке x равна 1/(1+x^2) для точек дифференцируемости.

LaTeX

$$$ \forall x, \ deriv (\arctan) x = \frac{1}{1+x^2}. $$$

Lean4

@[simp]
theorem deriv_arctan : deriv arctan = fun (x : ℝ) => 1 / (1 + x ^ 2) :=
  funext fun x => (hasDerivAt_arctan x).deriv

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

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

Разделы

Аффилиация

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