update — Mathlib

English

If f is meromorphic at z, then updating f at any value w and any coordinate e yields a meromorphic function at z.

Русский

Если f мероморфна в z, то обновленная функция будет мероморфна в z при любом значении w и любом e.

LaTeX

$$$MeromorphicAt f z \\to MeromorphicAt (Function.update f w e) z$$$

Lean4

@[fun_prop]
theorem update [DecidableEq 𝕜] {f : 𝕜 → E} {z} (hf : MeromorphicAt f z) (w e) :
    MeromorphicAt (Function.update f w e) z :=
  update_iff.mpr hf

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