differentiableAt_cos — Mathlib

English

Let cos be viewed as a complex-valued function on the complex plane; cos is differentiable at every point of the complex plane.

Русский

Пусть cos: ℂ → ℂ — комплекснозначная функция; косинус дифференцируем в каждой точке ℂ.

LaTeX

$$$\frac{d}{dz}\cos z \text{ существует for all } z \in \mathbb{C}$$$

Lean4

@[simp]
theorem differentiableAt_cos {x : ℂ} : DifferentiableAt ℂ cos x :=
  differentiable_cos x

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