Removable singularity theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove Riemann's removable singularity theorem: if f : ℂ → E is complex
differentiable in a punctured neighborhood of a point c and is bounded in a punctured neighborhood
of c (or, more generally, $f(z) - f(c)=o((z-c)^{-1})$), then it has a limit at c and the
function function.update f c (lim (𝓝[≠] c) f) is complex differentiable in a neighborhood of c.
Removable singularity theorem, weak version. If f : ℂ → E is differentiable in a punctured
neighborhood of a point and is continuous at this point, then it is analytic at this point.
Removable singularity theorem: if s is a neighborhood of c : ℂ, a function f : ℂ → E
is complex differentiable on s \ {c}, and $f(z) - f(c)=o((z-c)^{-1})$, then f redefined to be
equal to lim (𝓝[≠] c) f at c is complex differentiable on s.
Removable singularity theorem: if s is a punctured neighborhood of c : ℂ, a function
f : ℂ → E is complex differentiable on s, and $f(z) - f(c)=o((z-c)^{-1})$, then f redefined to
be equal to lim (𝓝[≠] c) f at c is complex differentiable on {c} ∪ s.
Removable singularity theorem: if s is a neighborhood of c : ℂ, a function f : ℂ → E
is complex differentiable and is bounded on s \ {c}, then f redefined to be equal to
lim (𝓝[≠] c) f at c is complex differentiable on s.
Removable singularity theorem: if a function f : ℂ → E is complex differentiable on a
punctured neighborhood of c and $f(z) - f(c)=o((z-c)^{-1})$, then f has a limit at c.
Removable singularity theorem: if a function f : ℂ → E is complex differentiable and
bounded on a punctured neighborhood of c, then f has a limit at c.
The Cauchy formula for the derivative of a holomorphic function.