English
Variant lemma: outside the support of D, the trailing coefficient equals the corresponding product with updated at those indices.
Русский
Лемма: вне опоры D завершающий коэффициент равен соответствующему произведению с обновлением на тех индексаx.
LaTeX
$$$\\text{meromorphicTrailingCoeffAt}\\left(\\prod^{\\mathrm{fin}}_{u} (\\cdot - u)^{D(u)}\\right) x = \\prod^{\\mathrm{fin}}_{u} (x - u)^{D(u)\\text{ обновлено}}$$$
Lean4
/-- Formulation of `MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin` as an
identity principle: Let `U` be a subset of `𝕜` and assume that `x ∈ U` is not an isolated point of
`U`. If function `f` and `g` are meromorphic at `x` and agree along a subset that is codiscrete
within `U`, then `f` and `g` agree in a punctured neighbourhood of `f`.
-/
theorem eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf : MeromorphicAt f x) (hg : MeromorphicAt g x)
(h₁x : x ∈ U) (h₂x : AccPt x (𝓟 U)) (h : f =ᶠ[codiscreteWithin U] g) : f =ᶠ[𝓝[≠] x] g :=
by
rw [eventuallyEq_iff_sub] at *
apply (hf.sub hg).eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin h₁x h₂x h
