sub — Mathlib

English

If hf and hg hold for f and g respectively, then f − g is analytic within the same neighborhood.

Русский

Если hf и hg выполняются для f и g, то f − g аналитична в той же окрестности.

LaTeX

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

Lean4

theorem sub (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (f - g) s := fun z hz =>
  (hf z hz).sub (hg z hz)

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