analyticOn_cosh — Mathlib

English

For any set in the complex plane, cosh is analytic on that set (since cosh is entire).

Русский

Для любого множества в плоскости комплексных чисел cosh аналитична на этом множестве (поскольку cosh является целой функцией).

LaTeX

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

Lean4

/-- The function `Complex.cosh` is complex analytic. -/
theorem analyticOn_cosh {s : Set ℂ} : AnalyticOn ℂ cosh s :=
  contDiff_cosh.contDiffOn.analyticOn

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