analyticOnNhd_sinh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Complex.analyticOnNhd_sinh

English

Sinh is analytic on nhds neighborhoods around points of any set.

Русский

Sinh аналитичен на окрестностях вокруг точек любого множества.

LaTeX

$$$\text{AnalyticOnNhd }\sinh s$$$

Lean4

/-- The function `Complex.sinh` is complex analytic. -/
theorem analyticOnNhd_sinh {s : Set ℂ} : AnalyticOnNhd ℂ sinh s := fun _ _ ↦ analyticAt_sinh

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru