deriv_tan_sub_id — Mathlib

English

If cos x ≠ 0, then the derivative of tan x − x at x is 1/cos^2 x − 1.

Русский

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

LaTeX

$$$\cos x \ne 0 \Rightarrow \dfrac{d}{dx}(\tan x - x) = \dfrac{1}{\cos^2 x} - 1$$$

Lean4

/-- The derivative of `tan x - x` is `1/(cos x)^2 - 1` away from the zeroes of cos. -/
theorem deriv_tan_sub_id (x : ℝ) (h : cos x ≠ 0) : deriv (fun y : ℝ => tan y - y) x = 1 / cos x ^ 2 - 1 :=
  HasDerivAt.deriv <| by simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg

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