109.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/109
[MRR19] J. Moreira, F.K. Richter, and D. Robertson, A proof of a sumset conjecture of Erdős, Annals of Math. 189 (2019), 605-652.

Imports (1)

theorem Erdos109.erdos_109 sorry line 43 source
depends on sorry what this means
Statement uses: Set, Nat, GT.gt, Real, Set.upperDensity, Set.univ, OfNat.ofNat, Exists, And, Set.Infinite, LE.le, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.