English
If f is differentiable within s at x and s has a unique differentiation point at x, then the Fréchet derivative within s of arctan(f) at x equals (1 / (1 + f(x)^2)) times the Fréchet derivative within s of f at x.
Русский
Если f дифференцируема внутри s в точке x, и в точке x существует единое различное касание (UniqueDiffWithinAt), то производная arctan(f) внутри s в x равна (1 / (1 + f(x)^2)) умноженному на производную f внутри s в x.
LaTeX
$$$fderivWithin_\mathbb{R}(\arctan( f))\; s\; x = \dfrac{1}{1 + f(x)^2}\; fderivWithin_\mathbb{R} f\; s\; x.$$$
Lean4
theorem fderivWithin_arctan (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun x => arctan (f x)) s x = (1 / (1 + f x ^ 2)) • fderivWithin ℝ f s x :=
hf.hasFDerivWithinAt.arctan.fderivWithin hxs
