From d7b78e8e330b11a5df59c9b6244d5b9416183cc1 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 14 Nov 2024 16:53:35 +0100
Subject: [PATCH] working

---
 Nevanlinna/meromorphicOn.lean                 | 29 +++++++++++++++++++
 ...n => stronglyMeromorphicOn_eliminate.lean} |  0
 2 files changed, 29 insertions(+)
 create mode 100644 Nevanlinna/meromorphicOn.lean
 rename Nevanlinna/{meromorphicOn_decompose.lean => stronglyMeromorphicOn_eliminate.lean} (100%)

diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
new file mode 100644
index 0000000..ac66cb9
--- /dev/null
+++ b/Nevanlinna/meromorphicOn.lean
@@ -0,0 +1,29 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn_divisor
+import Nevanlinna.stronglyMeromorphicOn
+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₁f : MeromorphicOn f U) :
+  (∃ 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
+    obtain ⟨w, hw⟩ := h₁U.nonempty
+    use ⟨w, hw⟩
+    exact h ⟨w, hw⟩
diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
similarity index 100%
rename from Nevanlinna/meromorphicOn_decompose.lean
rename to Nevanlinna/stronglyMeromorphicOn_eliminate.lean