Update divisor.lean

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 ℂ}