contDiff_arctan — Mathlib

English

The function arctan is ContDiff of any order.

Русский

Функция arctan обладает ContDiff любой степени.

LaTeX

$$$ \forall n, \ ContDiff \mathbb{R} n \ arctan. $$$

Lean4

theorem contDiff_arctan {n : WithTop ℕ∞} : ContDiff ℝ n arctan :=
  contDiff_iff_contDiffAt.2 fun x =>
    have : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
    tanPartialHomeomorph.contDiffAt_symm_deriv (by simpa) trivial (hasDerivAt_tan this) (contDiffAt_tan.2 this)

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