286.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/286
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Cr01] Croot, III, Ernest S., On unit fractions with denominators in short intervals. Acta Arith. (2001), 99-114.

Imports (1)

theorem Erdos286.erdos_286 sorry line 46 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, Filter.Eventually, Eq, HSub.hSub, HMul.hMul, HAdd.hAdd, Real.exp, Finset, Finset.card, Not, Membership.mem and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.