English
On a connected domain U, there exists a point with finite order iff every point has finite order.
Русский
На связном объединении U существует точка с конечным порядком тогда и только тогда, когда во всех точках порядок конечен.
LaTeX
$$$\\exists u\\in U:\\, meromorphicOrderAt f u \\neq \\top \\iff \\forall u\\in U:\\, meromorphicOrderAt f u \\neq \\top$$$
Lean4
/-- If a function is meromorphic on a set `U`, then for each point in `U`, it is analytic at nearby
points in `U`. When the target space is complete, this can be strengthened to analyticity at all
nearby points, see `MeromorphicAt.eventually_analyticAt`. -/
theorem eventually_analyticAt (h : MeromorphicOn f U) (hx : x ∈ U) : ∀ᶠ y in 𝓝[U \ { x }] x, AnalyticAt 𝕜 f y := by
/- At neighboring points in `U`, the function `f` is both meromorphic (by meromorphicity on `U`)
and continuous (thanks to the formula for a meromorphic function around the point `x`), so it is
analytic. -/
have : ∀ᶠ y in 𝓝[U \ { x }] x, ContinuousAt f y :=
by
have : U \ { x } ⊆ { x }ᶜ := by simp
exact nhdsWithin_mono _ this (h x hx).eventually_continuousAt
filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
exact (h y h'y.1).analyticAt hy
