English
If f1 is meromorphic on U and f2 agrees with f1 on codiscreteWithin U, then divisor equality holds after restricting to Uᶜ with open U.
Русский
Если f1 мероморфна на U и f2 совпадает с f1 на codiscreteWithin U, то при ограничении делитель совпадает.
LaTeX
$$$\text{MeromorphicOn}(f_1, U) \Rightarrow (f_1 =\!\!\!\!_{\text{codiscreteWithin }U} f_2) \Rightarrow \text{IsOpen}(U) \Rightarrow \text{divisor}(f_1, U) = \text{divisor}(f_2, U)$$$
Lean4
/-- If `f₁` is meromorphic on `U`, if `f₂` agrees with `f₁` on a codiscrete subset of `U` and outside of
`U`, then `f₁` and `f₂` induce the same divisors on `U`.
-/
theorem divisor_congr_codiscreteWithin_of_eqOn_compl {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U)
(h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : Set.EqOn f₁ f₂ Uᶜ) : divisor f₁ U = divisor f₂ U :=
by
ext x
by_cases hx : x ∈ U
· simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin_of_eqOn_compl h₁ h₂]
congr 1
apply meromorphicOrderAt_congr
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁
filter_upwards [h₁ x hx] with a ha
simp at ha
tauto
· simp [hx]
