arctan — Mathlib

English

If f has a derivative within a set s at x, then arctan ∘ f has a derivative within s at x with the same rule as HasDerivAt.

Русский

Если у f есть производная внутри множества s в x, то arctan(f) имеет производную внутри s в x по той же формуле, что и HasDerivAt.

LaTeX

$$$ \text{HasDerivWithinAt arctan}(f, f', s, x) \Rightarrow \text{HasDerivWithinAt } (x \mapsto \arctan(f(x))) \left( \frac{1}{1+f(x)^2} f' \right), s, x.$$$

Lean4

theorem arctan (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (fun x => arctan (f x)) (1 / (1 + f x ^ 2) * f') s x :=
  (Real.hasDerivAt_arctan (f x)).comp_hasDerivWithinAt x hf

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