Working…

Nevanlinna/meromorphicOn.lean

@@ -2,7 +2,6 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
-import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicOn
 import Nevanlinna.mathlibAddOn
 

Nevanlinna/meromorphicOn_divisor.lean

@@ -2,6 +2,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn
 import Nevanlinna.stronglyMeromorphicOn
 
 
@@ -183,17 +184,33 @@ theorem StronglyMeromorphicOn.analyticOnNhd
     tauto
   assumption
 
+
 theorem StronglyMeromorphicOn.support_divisor
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hU : IsPreconnected U)
+  (hU : IsConnected U)
   (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  (h₂f : ∃ u : U, f u ≠ 0) :
   U ∩ f⁻¹' {0} = (Function.support h₁f.meromorphicOn.divisor) := by
 
   ext u
   constructor
-  · sorry
+  · intro hu
+    unfold MeromorphicOn.divisor
+    simp [MeromorphicOn.order_ne_top hU h₁f h₂f ⟨u, hu.1⟩]
+    use hu.1
+    rw [(h₁f u hu.1).order_eq_zero_iff]
+    simp
+    exact hu.2
   · intro hu
     simp at hu
-    sorry
+    let A := h₁f.meromorphicOn.divisor.supportInU hu
+    constructor
+    · exact h₁f.meromorphicOn.divisor.supportInU hu
+    · simp
+      let B := (h₁f u A).order_eq_zero_iff.not
+      simp at B
+      rw [← B]
+      unfold MeromorphicOn.divisor at hu
+      simp [A] at hu
+      exact hu.1