English
Equating two meromorphic functions f and g near a point x is equivalent to them agreeing frequently or eventually in a punctured neighborhood.
Русский
Согласие двух мероморфных функций f и g в окрестности x эквивалентно частому/конечному согласию вне точки x.
LaTeX
$$$\text{frequently}\; (f=g) \iff f =^{\text{near}} g$$
Lean4
/-- Variant of the principle of isolated zeros: Let `U` be a subset of `𝕜` and assume that `x ∈ U` is
not an isolated point of `U`. If a function `f` is meromorphic at `x` and vanishes along a subset
that is codiscrete within `U`, then `f` vanishes in a punctured neighbourhood of `f`.
For a typical application, let `U` be a path in the complex plane and let `x` be one of the end
points. If `f` is meromorphic at `x` and vanishes on `U`, then it will vanish in a punctured
neighbourhood of `x`, which intersects `U` non-trivially but is not contained in `U`.
The assumption that `x` is not an isolated point of `U` is expressed as `AccPt x (𝓟 U)`. See
`accPt_iff_frequently` and `accPt_iff_frequently_nhdsNE` for useful reformulations.
-/
theorem eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin (hf : MeromorphicAt f x) (h₁x : x ∈ U)
(h₂x : AccPt x (𝓟 U)) (h : f =ᶠ[codiscreteWithin U] 0) : f =ᶠ[𝓝[≠] x] 0 :=
by
rw [← hf.frequently_zero_iff_eventuallyEq_zero]
apply ((accPt_iff_frequently_nhdsNE.1 h₂x).and_eventually (mem_codiscreteWithin_iff_forall_mem_nhdsNE.1 h x h₁x)).mp
filter_upwards
intro a
simp_rw [Pi.zero_apply]
rw [(by rfl : ({x | f x = 0} ∪ Uᶜ) a ↔ a ∈ {x | f x = 0} ∪ Uᶜ)]
simp_all
