analyticOn_cos — Mathlib

English

The function cos is analytic on any subset of the complex plane (cos is entire).

Русский

Функция cos аналитична на любом подмножестве ℂ (cos всю плоскость аналитична).

LaTeX

$$$\text{AnalyticOn }\cos s\quad\text{for all } s \subseteq \mathbb{C}$$$

Lean4

/-- The function `Complex.cos` is complex analytic. -/
theorem analyticOn_cos {s : Set ℂ} : AnalyticOn ℂ cos s :=
  contDiff_cos.contDiffOn.analyticOn

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