Source indexedlemma · leanprover/lean4:v4.32.0

divisor_support_rectangle_finite

PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:264 to 274

Mathematical statement

Exact Lean statement

lemma divisor_support_rectangle_finite (f : ℂ → ℂ) (z w : ℂ) :
    (MeromorphicOn.divisor f (Rectangle z w)).support.Finite

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma divisor_support_rectangle_finite (f : ℂ → ℂ) (z w : ℂ) :    (MeromorphicOn.divisor f (Rectangle z w)).support.Finite := by  let R : Set ℂ := Rectangle z w  let D := MeromorphicOn.divisor f R  have hR_compact : IsCompact R := by    exact IsCompact.reProdIm isCompact_uIcc isCompact_uIcc  have hfinite_inter :      (R ∩ D.support).Finite :=    MeromorphicOn.divisor_support_inter_compact_finite (f := f) (U := R) (K := R)      hR_compact subset_rfl  simpa [Set.inter_eq_right.mpr D.supportWithinDomain] using hfinite_inter