kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update divisor.lean

This commit is contained in:
Stefan Kebekus 2024-11-06 16:15:27 +01:00
parent 9d6801c329
commit a95c34fd05
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Nevanlinna/divisor.lean
View File

@ -87,5 +87,7 @@ theorem Divisor.finiteSupport
(hU : IsCompact U) (hU : IsCompact U)
(D : Divisor U) : (D : Divisor U) :
Set.Finite D.toFun.support := by Set.Finite D.toFun.support := by
apply IsCompact.finite
sorry · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
exact D.supportInU
· exact D.discreteSupport hU.isClosed