hasStrictDerivAt_tan — Mathlib

English

For all x with cos x ≠ 0, the derivative of tan at x is 1/cos^2 x.

Русский

Для всех x, при cos x ≠ 0, производная тангенса в точке x равна 1/cos^2 x.

LaTeX

$$$ \text{If } \cos x \neq 0, \quad \dfrac{d}{dx} \tan x = \dfrac{1}{\cos^2 x}. $$$

Lean4

theorem hasStrictDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x :=
  mod_cast (Complex.hasStrictDerivAt_tan (by exact mod_cast h)).real_of_complex

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