English
If f is meromorphic on U and x ∈ U, then in a punctured neighborhood of x the global normal form on U equals the local normal form at x.
Русский
Если f мероморфна на U и x ∈ U, то в пунктированной окрестности x глобальная нормальная форма на U совпадает с локальной нормальной формой в точке x.
LaTeX
$$$toMeromorphicNFOn\ f\ U =^{{\mathcal{N}_{x}^{\neq}}}\ toMeromorphicNFAt\ f\ x\ x$$$
Lean4
/-- If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
and conversion to normal form on `U` agree in a neighborhood of `x`.
-/
theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds (hf : MeromorphicOn f U) (hx : x ∈ U) :
toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x :=
by
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
· exact (hf.toMeromorphicNFOn_eq_self_on_nhdsNE hx).trans (hf x hx).eq_nhdsNE_toMeromorphicNFAt
· simp [toMeromorphicNFOn, hf, hx]
