English
If f and g agree in a neighborhood of x, then f and g have the same meromorphic-in-normal-form status at x.
Русский
Если f и g совпадают в окрестности x, то они имеют одинаковый статус мероморфности в нормальной форме в точке x.
LaTeX
$$$(f =^{nhds\ x} g) \Rightarrow (MeromorphicNFAt\ f\ x \iff MeromorphicNFAt\ g\ x)$$$
Lean4
/-- Meromorphicity in normal form is a local property. -/
theorem meromorphicNFAt_congr {g : 𝕜 → E} (hfg : f =ᶠ[𝓝 x] g) : MeromorphicNFAt f x ↔ MeromorphicNFAt g x :=
by
constructor
· rintro (h | ⟨n, h, h₁h, h₂h, h₃h⟩)
· exact .inl (hfg.symm.trans h)
· exact .inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩
· rintro (h | ⟨n, h, h₁h, h₂h, h₃h⟩)
· exact .inl (hfg.trans h)
· exact .inr ⟨n, h, h₁h, h₂h, hfg.trans h₃h⟩
