From 9d6801c329b598235d4a4719ba23df901a9c15e6 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 6 Nov 2024 16:08:17 +0100
Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/divisor.lean | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index aa3c5d4..e498d42 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -23,6 +23,41 @@ instance
 attribute [coe] Divisor.toFun
 
 
+theorem Divisor.discreteSupport
+  {U : Set ℂ}
+  (hU : IsClosed U)
+  (D : Divisor U) :
+  DiscreteTopology D.toFun.support := by
+  apply discreteTopology_subtype_iff.mpr
+  intro x hx
+  apply inf_principal_eq_bot.mpr
+  by_cases h₁x : x ∈ U
+  · let A := D.locallyFiniteInU x h₁x
+    refine mem_nhdsWithin.mpr ?_
+    rw [eventuallyEq_nhdsWithin_iff] at A
+    obtain ⟨U, h₁U, h₂U, h₃U⟩ := eventually_nhds_iff.1 A
+    use U
+    constructor
+    · exact h₂U
+    · constructor
+      · exact h₃U
+      · intro y hy
+        let C := h₁U y hy.1 hy.2
+        tauto
+  · refine mem_nhdsWithin.mpr ?_
+    use Uᶜ
+    constructor
+    · simpa
+    · constructor
+      · tauto
+      · intro y _
+        let A := D.supportInU
+        simp at A
+        simp
+        exact False.elim (h₁x (A x hx))
+
+
+
 theorem Divisor.closedSupport
   {U : Set ℂ}
   (hU : IsClosed U)