arctan — Mathlib

English

Let f: E → ℝ be differentiable within a set s at x with derivative f'. Then the derivative within s of arctan(f(x)) equals (1 / (1 + f(x)^2)) • f'(x).

Русский

Пусть f: E → ℝ дифференцируема в пункте x на множества s; тогда производная arctan(f(x)) внутри s равна (1 / (1 + f(x)^2)) • f'(x).

LaTeX

$$$fderivWithin_\mathbb{R}(\arctan \circ f)\; s\; x = \dfrac{1}{1 + f(x)^2} \; fderivWithin_\mathbb{R} f\; s\; x.$$$

Lean4

theorem arctan (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x :=
  (hasDerivAt_arctan (f x)).comp_hasFDerivWithinAt x hf

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