derivWithin_arctan — Mathlib

English

For differentiable f, deriv of arctan(f(x)) equals (1/(1+f(x)^2))·f'(x).

Русский

Для дифференцируемой f производная arctan(f(x)) равна (1/(1+f(x)^2))·f'(x).

LaTeX

$$$ \text{deriv arctan }(f(x)) = \frac{1}{1+f(x)^2} \cdot f'(x). $$$

Lean4

theorem derivWithin_arctan (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => arctan (f x)) s x = 1 / (1 + f x ^ 2) * derivWithin f s x :=
  hf.hasDerivWithinAt.arctan.derivWithin hxs

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