sub — Mathlib

English

Let f and g be meromorphic at x. Then f − g is meromorphic at x.

Русский

Пусть f и g мероморфны в x. Тогда f − g мероморфна в x.

LaTeX

$$$MeromorphicAt f x \\to MeromorphicAt g x \\to MeromorphicAt (fun z \\mapsto f z - g z) x$$$

Lean4

@[fun_prop]
theorem sub {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (f - g) x :=
  by
  convert hf.add hg.neg using 1
  ext1 z
  simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]

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