update_iff — Mathlib

English

For any w and e, MeromorphicAt f z implies MeromorphicAt (Function.update f w e) z (when a DecidableEq structure is available).

Русский

При наличии структуры DecidableEq, для любых w и e из 𝕜, мероморфность f в z влечёт мероморфность обновленной функции в z.

LaTeX

$$$\\text{[DecidableEq 𝕜]} \\Rightarrow MeromorphicAt f z \\to MeromorphicAt (Function.update f w e) z$$$

Lean4

@[simp]
theorem update_iff [DecidableEq 𝕜] {f : 𝕜 → E} {z w : 𝕜} {e : E} :
    MeromorphicAt (Function.update f w e) z ↔ MeromorphicAt f z :=
  meromorphicAt_congr (Function.update_eventuallyEq_nhdsNE f w z e)

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