Source indexedlemma · leanprover/lean4:v4.32.0

riemannZeta.zeroes_on_Compact_finite

PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions · PrimeNumberTheoremAnd/IEANTN/ZetaDefinitions.lean:61 to 70

Mathematical statement

Exact Lean statement

lemma riemannZeta.zeroes_on_Compact_finite {S : Set ℂ} (hS1 : IsCompact S) (hS2 : 1 ∉ 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) (hS2 : 1 ∉ S) :    (S ∩ zeroes : Set ℂ).Finite := by  have sub := Set.subset_compl_singleton_iff.mpr hS2  refine IsCompact.finite ?_ ?_  · have := riemannZeta_analyticOn_compl_one.continuousOn.mono sub      |>.preimage_isClosed_of_isClosed (t := {0}) hS1.isClosed isClosed_singleton    exact hS1.of_isClosed_subset this Set.inter_subset_left  · rw [Set.inter_comm]    exact IsDiscrete.mono (isDiscrete_of_codiscreteWithin zeroes_codiscreteWithin_compl_one)      <| Set.inter_subset_inter_right zeroes sub