analyticOnNhd_cos — Mathlib

English

The cosine function is analytic on any neighborhood in the complex plane around any point of a set.

Русский

Косинус аналитичен на любой окрестности в комплексной плоскости вокруг любой точки множества.

LaTeX

$$$\text{AnalyticOnNhd }\cos s\, \text{ for any } s \subseteq \mathbb{C}$$$

Lean4

/-- The function `Complex.cos` is complex analytic. -/
theorem analyticOnNhd_cos {s : Set ℂ} : AnalyticOnNhd ℂ cos s := fun _ _ ↦ analyticAt_cos

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