fun_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem fun_sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (fun z ↦ f z - g z) x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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