From 1a8bde51ebc59c7c7962ad751449cc663412f24a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 17 Sep 2024 11:03:44 +0200
Subject: [PATCH] Update divisor.lean

---
 Nevanlinna/divisor.lean | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index 728cddd..ee81b3f 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -23,15 +23,31 @@ noncomputable def Divisor.n
 noncomputable def Divisor.N_trunk
   (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
 
-theorem Divisor.compactSupport
+
+theorem Divisor.support_cap_closed
   (D : Divisor)
   {U : Set ℂ}
-  (h₁U : IsCompact U)
-  (h₂U : Function.support D ⊆ U) :
-  Set.Finite (Function.support D) := by
+  (h₁U : IsClosed U) :
+  IsClosed (U ∩ D.toFun.support) := by
   sorry
 
 
+theorem Divisor.support_cap_compact
+  (D : Divisor)
+  {U : Set ℂ}
+  (h₁U : IsCompact U) :
+  Set.Finite (U ∩ (Function.support D)) := by
+
+  apply IsCompact.finite
+  -- Target set is compact
+  apply h₁U.of_isClosed_subset
+  apply D.support_cap_closed h₁U.isClosed
+  exact Set.inter_subset_left
+  -- Target set is discrete
+  apply DiscreteTopology.of_subset D.discreteSupport
+  exact Set.inter_subset_right
+
+
 noncomputable def AnalyticOn.zeroDivisor
   {f : ℂ → ℂ}
   {U : Set ℂ}