neg

Mathlib.Analysis.Analytic.Constructions

URI: https://scilib.ai/kg/mathlib#AnalyticOn.neg

English

If f and g are AnalyticOnNhd 𝕜, then f + g is AnalyticOnNhd 𝕜.

Русский

Если f и g аналитичны в окрестности, то f + g аналитична.

LaTeX

$$$\text{AnalyticOnNhd}(f, s) \land \text{AnalyticOnNhd}(g, s) \Rightarrow \text{AnalyticOnNhd}(f + g, s)$$$

Lean4

theorem neg (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s := fun z hz ↦ (hf z hz).neg

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

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

Разделы

Аффилиация

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