fun_const_smul — Mathlib

English

If f and g are analytic on s, then x ↦ f(x) + g(x) is analytic on s.

Русский

Если функции f и g аналитичны на s, то функция x ↦ f(x) + g(x) аналитична на s.

LaTeX

$$$\text{AnalyticOn}(f, s) \land \text{AnalyticOn}(g, s) \Rightarrow \text{AnalyticOn}(x \mapsto f(x) + g(x), s)$$$

Lean4

@[fun_prop]
theorem fun_const_smul (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fun z ↦ c • f z) x :=
  let ⟨_, hpf⟩ := hf
  hpf.const_smul.analyticAt

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