const_smul

Mathlib.Analysis.Analytic.Constructions

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

English

If f is analytic at x, then c·f is analytic at x.

Русский

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

LaTeX

$$$\text{AnalyticAt}(f, x) \Rightarrow \text{AnalyticAt}(c \cdot f, x)$$$

Lean4

theorem const_smul (hf : HasFPowerSeriesAt f pf x) : HasFPowerSeriesAt (c • f) (c • pf) x :=
  let ⟨_, hrf⟩ := hf
  hrf.const_smul.hasFPowerSeriesAt

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

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

Разделы

Аффилиация

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