hasStrictDerivAt_cos — Mathlib

English

The cosine function has a strict derivative with value -sin x.

Русский

У косинуса строгая производная, равная − sin x.

LaTeX

$$$$\text{HasStrictDerivAt}(\cos, -\sin x, x).$$$$

Lean4

/-- The complex cosine function is everywhere strictly differentiable, with the derivative
`-sin x`. -/
theorem hasStrictDerivAt_cos (x : ℂ) : HasStrictDerivAt cos (-sin x) x :=
  by
  simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]
  convert
    (((hasStrictDerivAt_id x).mul_const I).cexp.add ((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp).mul_const
      (2 : ℂ)⁻¹ using
    1
  simp only [id]
  ring

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