contDiffAt_tan — Mathlib

English

The function arctan is continuously differentiable (ContDiff) of all orders.

Русский

Функция arctan имеет непрерывно дифференцируемость во всех порядках.

LaTeX

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

Lean4

@[simp]
theorem contDiffAt_tan {n : WithTop ℕ∞} {x : ℝ} : ContDiffAt ℝ n tan x ↔ cos x ≠ 0 :=
  ⟨fun h => continuousAt_tan.1 h.continuousAt, fun h => (Complex.contDiffAt_tan.2 <| mod_cast h).real_of_complex⟩

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