analyticOnNhd_cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Real.analyticOnNhd_cos

English

cos is analytic on neighborhoods of points in s.

Русский

cos аналитична на окрестностях точек из s.

LaTeX

$$$\\cos(x+h) = \\cos x \\cos h - \\sin x \\sin h$$$

Lean4

/-- The function `Real.cos` is real analytic. -/
theorem analyticOnNhd_cos {s : Set ℝ} : AnalyticOnNhd ℝ cos s := fun _ _ ↦ analyticAt_cos

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

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

Разделы

Аффилиация

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