31.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/31
[Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137.
[Er59] Erdős, P., Über einige Probleme der additiven Zahlentheorie. Sammelband zu Ehren des 250. Geburtstages Leonhard Eulers (1959), 116-119.
[Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244.
[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[Lo54] Lorentz, G. G., On a problem of additive number theory. Proc. Amer. Math. Soc. (1954), 838-841.

Imports (1)

theorem Erdos31.erdos_31 sorry line 51 source
depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, Exists, And, Set.HasDensity, OfNat.ofNat, Real, Set.univ, Filter.Eventually, Membership.mem, HAdd.hAdd, Set.add, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.