English
If f is meromorphic on U and x ∈ U, then the global normal form on U and f agree in a punctured neighborhood of x (i.e., away from x).
Русский
Если f мероморфна на U и x ∈ U, то глобальная нормальная форма на U совпадает с f в окружающей окрестности x за исключением точки x.
LaTeX
$$$toMeromorphicNFOn\ f\ U =^{{\mathcal{N}_{x}^{\neq}}}\ f$ при некоторых условиях на x; компактная формулировка:$$
Lean4
/-- If `f` is meromorphic on `U` and `x ∈ U`, then `f` and its conversion to normal
form on `U` agree in a punctured neighborhood of `x`.
-/
theorem toMeromorphicNFOn_eq_self_on_nhdsNE (hf : MeromorphicOn f U) (hx : x ∈ U) :
toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f :=
by
filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha
rcases ha with ha | ha
· simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]
· simp only [Set.mem_compl_iff] at ha
simp [toMeromorphicNFOn, ha, hf]
