Update holomorphic_zero.lean

This commit is contained in:
Stefan Kebekus 2024-08-16 20:24:24 +02:00
parent d0cd033d5c
commit f9f177e7b9
1 changed files with 19 additions and 0 deletions

View File

@ -115,6 +115,25 @@ theorem zeroDivisor_support_iff
assumption assumption
example
{f : }
{U : Set }
(hU : IsPreconnected U)
(h₁f : AnalyticOn f U)
(h₂f : ∃ z ∈ U, f z ≠ 0) :
∀ (hz : z ∈ U), (h₁f z hz).order ≠ := by
by_contra H
push_neg at H
obtain ⟨z', hz'⟩ := H
rw [AnalyticAt.order_eq_top_iff] at hz'
let A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z'
rw [AnalyticAt.frequently_eq_iff_eventually_eq] at A
let B := A hz'
sorry
theorem discreteZeros theorem discreteZeros
{f : } : {f : } :
DiscreteTopology (Function.support (zeroDivisor f)) := by DiscreteTopology (Function.support (zeroDivisor f)) := by