Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorZeroIndex₀_fiber_finite

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorFiber.lean:54 to 70

Mathematical statement

Exact Lean statement

theorem divisorZeroIndex₀_fiber_finite (f : ℂ → ℂ) (z₀ : ℂ) :
    ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | divisorZeroIndex₀_val p = z₀} :
      Set _).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem divisorZeroIndex₀_fiber_finite (f : ℂ → ℂ) (z₀ : ℂ) :    ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | divisorZeroIndex₀_val p = z₀} :      Set _).Finite := by  have hsub :      ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | divisorZeroIndex₀_val p = z₀} : Set _)        ⊆ ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | ‖divisorZeroIndex₀_val p‖ ≤ ‖z₀‖} :          Set _) := by    intro p hp    have : divisorZeroIndex₀_val p = z₀ := hp    simp [this]  have hfin :      ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | ‖divisorZeroIndex₀_val p‖ ≤ ‖z₀‖} :        Set _).Finite := by    have : Metric.closedBall (0 : ℂ) ‖z₀‖ ⊆ (Set.univ : Set ℂ) := by simp    simpa using (divisorZeroIndex₀_norm_le_finite (f := f) (U := (Set.univ : Set ℂ))      (B := ‖z₀‖) this)  exact hfin.subset hsub