English
If f is meromorphic on U, and f agrees with g on a codiscrete subset of U and outside U, then g is meromorphic on U.
Русский
Если f мероморфна на U, и f совпадает с g на кодискретной подмножестве U и вне U, тогда g мероморфна на U.
LaTeX
$$$MeromorphicOn f U \rightarrow (f =^{{codiscreteWithin U}} g) \rightarrow Set.EqOn f g U^c \rightarrow MeromorphicOn g U$$$
Lean4
/-- If `f` is meromorphic on an open set `U`, if `g` agrees with `f` on a codiscrete subset of `U`, then
`g` is also meromorphic on `U`.
-/
theorem congr_codiscreteWithin (hf : MeromorphicOn f U) (h₁ : f =ᶠ[codiscreteWithin U] g) (h₂ : IsOpen U) :
MeromorphicOn g U := by
intro x hx
apply (hf x hx).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
