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