38.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

Reference:

erdosproblems.com/38
[Er56](Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137.)

Imports (1)

theorem Erdos38.erdos_38 sorry line 56 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Set, Nat, And, Not, Set.IsWeakAddBasis, Real, LT.lt, OfNat.ofNat, GT.gt, schnirelmannDensity, Classical.propDecidable, Membership.mem, GE.ge, Set.ncard, Inter.inter, Set.Ioc, Union.union and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.