From a95c34fd056c303885963c1e79d541a840a5eff0 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 6 Nov 2024 16:15:27 +0100
Subject: [PATCH] Update divisor.lean

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

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index e498d42..8e74b25 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -87,5 +87,7 @@ theorem Divisor.finiteSupport
   (hU : IsCompact U)
   (D : Divisor U) :
   Set.Finite D.toFun.support := by
-
-  sorry
+  apply IsCompact.finite
+  · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
+    exact D.supportInU
+  · exact D.discreteSupport hU.isClosed