mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: Bergelson's Intersectivity Lemma

Open YaelDillies opened this issue 1 year ago • 4 comments

Prove a weak version of the Bergelson intersectivity lemma. The proof gives the strong version, but we need natural density to state it. This is a prerequisite to Tao and Ziegler's recent paper Infinite partial sumsets in the primes.

  • [x] depends on: #14421
  • [x] depends on: #14423

See https://github.com/leanprover-community/mathlib/pull/18732

Open in Gitpod

YaelDillies avatar Mar 04 '24 04:03 YaelDillies