hasDerivAt_cos — Mathlib

English

The cosine function is differentiable with derivative -sin x, i.e., hasDerivAt cos (-sin x) x.

Русский

Косинус дифференцируем, производная равна − sin x, i.e., hasDerivAt cos (−sin x) x.

LaTeX

$$$$\forall x, \; \text{HasDerivAt}(\cos, -\sin x, x).$$$$

Lean4

/-- The complex cosine function is everywhere differentiable, with the derivative `-sin x`. -/
theorem hasDerivAt_cos (x : ℂ) : HasDerivAt cos (-sin x) x :=
  (hasStrictDerivAt_cos x).hasDerivAt

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