Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.mem_divisorZeroIndex₀_fiberFinset_iff_val_mem_ball

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorFiber.lean:156 to 169

Mathematical statement

Exact Lean statement

lemma mem_divisorZeroIndex₀_fiberFinset_iff_val_mem_ball
    {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}
    (hε : 0 < ε)
    (hball :
      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})
    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) :
    p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀ ↔ divisorZeroIndex₀_val p ∈ Metric.ball z₀ ε

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma mem_divisorZeroIndex₀_fiberFinset_iff_val_mem_ball    {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hε : 0 < ε)    (hball :      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) :    p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀ ↔ divisorZeroIndex₀_val p ∈ Metric.ball z₀ ε := by  constructor  · intro hp    have : divisorZeroIndex₀_val p = z₀ :=      (mem_divisorZeroIndex₀_fiberFinset (f := f) (z₀ := z₀) p).1 hp    simpa [this] using (Metric.mem_ball_self hε : z₀ ∈ Metric.ball z₀ ε)  · intro hp    exact mem_divisorZeroIndex₀_fiberFinset_of_val_mem_ball (f := f) (z₀ := z₀) (ε := ε) hball p hp