contDiff_sin — Mathlib

English

The function sin is infinitely differentiable in the complex sense; in particular sin is ContDiff of any order.

Русский

Функция sin гладкая в комплексном смысле; синус гладкая любой порядок (ContDiff).

LaTeX

$$$$\forall n,\; \text{ContDiff } \mathbb{C} \; n \; \sin.$$$$

Lean4

@[fun_prop]
theorem contDiff_sin {n} : ContDiff ℂ n sin :=
  (((contDiff_neg.mul contDiff_const).cexp.sub (contDiff_id.mul contDiff_const).cexp).mul contDiff_const).div_const _

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