English
A simplified version of divisor congruence on codiscreteWithin.
Русский
Упрощённая версия конгруэнтности делителя на codiscreteWithin.
LaTeX
$$$\text{MeromorphicOn}(f_1, U) \Rightarrow (f_1 =\!\!\!\!_{\text{codiscreteWithin }U} f_2) \Rightarrow \text{divisor}(f_1, U) = \text{divisor}(f_2, U)$$$
Lean4
/-- If `f₁` is meromorphic on an open set `U`, if `f₂` agrees with `f₁` on a codiscrete subset of `U`,
then `f₁` and `f₂` induce the same divisors on`U`.
-/
theorem divisor_congr_codiscreteWithin {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U)
(h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : IsOpen U) : divisor f₁ U = divisor f₂ U :=
by
ext x
by_cases hx : x ∈ U
· simp only [hf₁, hx, divisor_apply, hf₁.congr_codiscreteWithin h₁ h₂]
congr 1
apply meromorphicOrderAt_congr
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁
have : U ∈ 𝓝[≠] x := by
apply mem_nhdsWithin.mpr
use U, h₂, hx, Set.inter_subset_left
filter_upwards [this, h₁ x hx] with a h₁a h₂a
simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and] at h₂a
tauto
· simp [hx]
