Update meromorphicOn.lean

Nevanlinna/meromorphicOn.lean

@@ -54,6 +54,44 @@ theorem MeromorphicOn.open_of_order_eq_top
     · exact isOpen_induced h₂t'
     · exact h₃t'
 
+theorem MeromorphicOn.open_of_order_neq_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : MeromorphicOn f U) :
+  IsOpen { u : U | (h₁f u.1 u.2).order ≠ ⊤ } := by
+
+  apply isOpen_iff_forall_mem_open.mpr
+  intro z hz
+  simp at hz
+
+  let A := (h₁f z.1 z.2).eventually_eq_zero_or_eventually_ne_zero
+  rcases A with h|h
+  · rw [← (h₁f z.1 z.2).order_eq_top_iff] at h
+    tauto
+  · let A := (h₁f z.1 z.2).eventually_analyticAt
+    let B := Filter.Eventually.and h A
+    rw [eventually_nhdsWithin_iff] at B
+    rw [eventually_nhds_iff] at B
+    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := B
+    let t : Set U := Subtype.val ⁻¹' t'
+    use t
+    constructor
+    · intro w hw
+      simp
+      by_cases h₁w : w = z
+      · rwa [h₁w]
+      · let B := h₁t' w hw
+        simp at B
+        have : (w : ℂ) ≠ (z : ℂ) := by exact Subtype.coe_ne_coe.mpr h₁w
+        let C := B this
+        let D := C.2.order_eq_zero_iff.2 C.1
+        rw [C.2.meromorphicAt_order, D]
+        simp
+    · constructor
+      · exact isOpen_induced h₂t'
+      · exact h₃t'
+
+
 theorem MeromorphicOn.order_ne_top
   {f : ℂ → ℂ}
   {U : Set ℂ}