analyticOnNhd_cosh — Mathlib

English

The complex hyperbolic cosine is analytic everywhere; in particular, cosh is holomorphic on the complex plane and hence analytic on any subset.

Русский

Комплексный гиперболический косинус аналитичен повсеместно; следовательно, cosh голоморфна на всей плоскости комплексных чисел и аналитична на любом подмножестве.

LaTeX

$$$\cosh: \mathbb{C} \to \mathbb{C}$ is holomorphic on $\mathbb{C}$.$$

Lean4

/-- The function `Complex.cosh` is complex analytic. -/
theorem analyticOnNhd_cosh {s : Set ℂ} : AnalyticOnNhd ℂ cosh s := fun _ _ ↦ analyticAt_cosh

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