hasStrictDerivAt_tan — Mathlib

English

If cos x ≠ 0, then tan has a strict derivative at x and it is 1/cos(x)^2.

Русский

Если cos x ≠ 0, то тангенс имеет строгую производную в точке x и она равна 1 / cos(x)^2.

LaTeX

$$$$ \text{HasStrictDerivAt}(\tan, 1/\cos^2 x, x) \quad \text{if } \cos x \neq 0. $$$$

Lean4

theorem hasStrictDerivAt_tan {x : ℂ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x :=
  by
  convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
  rw_mod_cast [← sin_sq_add_cos_sq x]
  ring

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