hasDerivAt_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

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

English

The derivative of arctan exists everywhere and equals 1/(1+x^2).

Русский

Дифференцируемость arctan везде и производная равна 1/(1+x^2).

LaTeX

$$$ \forall x \in \mathbb{R}, \ HasDerivAt arctan (1/(1+x^2)) x. $$$

Lean4

theorem hasDerivAt_arctan (x : ℝ) : HasDerivAt arctan (1 / (1 + x ^ 2)) x :=
  (hasStrictDerivAt_arctan x).hasDerivAt

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

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

Разделы

Аффилиация

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