fun_add — Mathlib

English

If f and g are analytic at x, then f+g is analytic at x.

Русский

Если функции f и g аналитичны в точке x, то сумма f+g аналитична в x.

LaTeX

$$$AnalyticAt\\ 𝕜 f x \\land AnalyticAt\\ 𝕜 g x \\Rightarrow AnalyticAt\\ 𝕜 (f+g) x$$$

Lean4

@[fun_prop]
theorem fun_add (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun z ↦ f z + g z) x :=
  let ⟨_, hpf⟩ := hf
  let ⟨_, hqf⟩ := hg
  (hpf.add hqf).analyticAt

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