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

Update analyticOn_zeroSet.lean

This commit is contained in:
Stefan Kebekus 2024-08-20 17:45:42 +02:00
parent 6d0870d533
commit 1160beac5e
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/analyticOn_zeroSet.lean
View File

@ -359,13 +359,10 @@ theorem AnalyticOnCompact.eliminateZeros
let A₁ := ι⁻¹' (U ∩ f⁻¹' {0}) let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
have t₁ : (U ∩ f⁻¹' {0}).Finite := by
sorry
have : A₁.Finite := by have : A₁.Finite := by
apply Set.Finite.preimage apply Set.Finite.preimage
exact Set.injOn_subtype_val exact Set.injOn_subtype_val
exact t₁ exact finiteZeros h₁U h₂U h₁f h₂f
let A := this.toFinset let A := this.toFinset
let n : ℂ → ℕ := by let n : ℂ → ℕ := by
@ -375,7 +372,12 @@ theorem AnalyticOnCompact.eliminateZeros
· exact 0 · exact 0
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
sorry intro a _
dsimp [n]
simp
rw [eq_comm]
apply XX h₁U
exact h₂f
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
use g use g