From 8bff0c782b3d5a2a4c3ae26eb0869e3581ee648a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 15 Nov 2024 09:01:55 +0100
Subject: [PATCH] Minor update

---
 Nevanlinna/meromorphicOn.lean                   |  3 ++-
 Nevanlinna/stronglyMeromorphicOn_eliminate.lean | 10 ----------
 2 files changed, 2 insertions(+), 11 deletions(-)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index ac66cb9..d88a1c9 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -14,13 +14,14 @@ theorem MeromorphicOn.order_ne_top
   {U : Set ℂ}
   (h₁U : IsConnected U)
   (h₁f : MeromorphicOn f U) :
-  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order ≠ ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order ≠ ⊤) := by
+  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
 
   constructor
   · intro h
     obtain ⟨h₁z₀, h₂z₀⟩ := h
     intro hz
 
+
     sorry
 
   · intro h
diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index 691fc76..a63406a 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -10,16 +10,6 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
-theorem MeromorphicOn.order_ne_top
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsConnected U)
-  (h₂U : IsCompact U)
-  (h₁f : MeromorphicOn f U)
-  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
-  ∀ hz : z ∈ U, (h₁f z hz).order ≠ ⊤ := by
-
-  sorry
 
 
 theorem MeromorphicOn.decompose