Source indexedlemma · leanprover/lean4:v4.32.0

riemannZeta.zeroes_on_Compact_finite'

PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions · PrimeNumberTheoremAnd/IEANTN/ZetaDefinitions.lean:90 to 97

Mathematical statement

Exact Lean statement

lemma riemannZeta.zeroes_on_Compact_finite' {S : Set ℂ} (hS1 : IsCompact S) :
    (S ∩ zeroes : Set ℂ).Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma riemannZeta.zeroes_on_Compact_finite' {S : Set ℂ} (hS1 : IsCompact S) :    (S ∩ zeroes : Set ℂ).Finite := by  obtain ⟨ε, hε, hball⟩ := riemannZeta_no_zeroes_near_one  have : S ∩ zeroes ⊆ (S ∩ (Metric.ball 1 ε)ᶜ) ∩ zeroes :=    fun s ⟨hs, hz⟩ ↦ ⟨⟨hs, fun hmem ↦ hball s hmem hz⟩, hz⟩  refine Set.Finite.subset (zeroes_on_Compact_finite ?_ ?_) this  · exact hS1.inter_right Metric.isOpen_ball.isClosed_compl  · exact fun ⟨_, h⟩ ↦ h (Metric.mem_ball_self hε)