const_smul

Mathlib.Analysis.Analytic.Constructions

URI: https://scilib.ai/kg/mathlib#AnalyticWithinAt.const_smul

English

If f and g are analytic at x, then z ↦ f(z) − g(z) is analytic at x.

Русский

Если f и g аналитичны в x, то z ↦ f(z) − g(z) аналитично в x.

LaTeX

$$$\text{AnalyticAt}(f, x) \land \text{AnalyticAt}(g, x) \Rightarrow \text{AnalyticAt}(z \mapsto f(z) - g(z), x)$$$

Lean4

theorem const_smul (hf : AnalyticWithinAt 𝕜 f s x) : AnalyticWithinAt 𝕜 (c • f) s x :=
  let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticWithinAt

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

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

Разделы

Аффилиация

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