From 551b4a2463a05d475f6b0f7578f4aa0ba538045a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 1 Oct 2024 06:51:18 +0200
Subject: [PATCH] Update divisor.lean

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

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index e5ddd49..e55ffaf 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -11,6 +11,7 @@ open Real Filter MeasureTheory intervalIntegral
 
 structure Divisor where
   toFun : ℂ → ℤ
+  -- This is not what we want. We want: locally finite
   discreteSupport : DiscreteTopology (Function.support toFun)
 
 instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
@@ -32,6 +33,29 @@ noncomputable def Divisor.N_trunk
   (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
 
 
+theorem Divisor.support_cap_closed₁
+  {S U : Set ℂ}
+  (hS : DiscreteTopology S)
+  (hU : IsClosed U) :
+  IsClosed (U ∩ S) := by
+
+  rw [← isOpen_compl_iff]
+  rw [isOpen_iff_forall_mem_open]
+  intro x hx
+  by_cases h₁x : x ∈ U
+  · simp at hx
+
+
+    sorry
+  · use Uᶜ
+    constructor
+    · simp
+    · constructor
+      · exact IsClosed.isOpen_compl
+      · assumption
+
+
+
 theorem Divisor.support_cap_closed
   (D : Divisor)
   {U : Set ℂ}