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

Update stronglyMeromorphicOn_eliminate.lean

Browse Source
This commit is contained in:
Stefan Kebekus 2024-11-26 14:14:03 +01:00
parent 092bfd85a3
commit 46740a0f17
1 changed files with 2 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Nevanlinna/stronglyMeromorphicOn_eliminate.lean
View File

@ -304,11 +304,8 @@ theorem MeromorphicOn.decompose₃
∧ (∀ u : U, g u ≠ 0)
∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by
have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
apply MeromorphicOn.order_ne_top h₂U h₁f h₂f
have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
exact h₁f.meromorphicOn.divisor.finiteSupport h₁U
have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f
have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor
let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset