hasDerivAt_arctan'

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

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

English

The derivative of arctan can be written as (1+x^2)^{-1} at every x.

Русский

Производная arctan записывается как (1+x^2)^{-1} в любой точке.

LaTeX

$$$ \text{theorem hasDerivAt_arctan' } (x) : \ HasDerivAt arctan ( (1+x^2)^{-1} ) x. $$$

Lean4

theorem hasDerivAt_arctan' (x : ℝ) : HasDerivAt arctan (1 + x ^ 2)⁻¹ x :=
  one_div (1 + x ^ 2) ▸ hasDerivAt_arctan x

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

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

Разделы

Аффилиация

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