sub — Mathlib

English

If f and g are analytic within at s around x, then their difference f − g is analytic within at s around x.

Русский

Если функции f и g аналитичны внутри области s около точки x, то их разность f − g аналитична внутри той же области.

LaTeX

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

Lean4

theorem sub (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) : AnalyticWithinAt 𝕜 (f - g) s x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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