add

Mathlib.Analysis.Analytic.Constructions

URI: https://scilib.ai/kg/mathlib#AnalyticAt.add

English

If f is analytic at x, then -f is analytic at x.

Русский

Если f аналитично в x, то -f аналитично в x.

LaTeX

$$$AnalyticAt\\ 𝕜 f x \\Rightarrow AnalyticAt\\ 𝕜 (-f) x$$$

Lean4

@[fun_prop]
theorem add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f + g) x :=
  hf.fun_add hg

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

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

Разделы

Аффилиация

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