658.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/658
[Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537.
[FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique (1991), 64-119.
[So04] Solymosi, J., A Note on a Question of Erdős and Graham. Combinatorics, Probability and Computing (2004), 263–267.

Imports (1)

theorem Erdos658.erdos_658 sorry line 55 source
depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, Prod, LE.le, SProd.sprod, Finset.Icc, HMul.hMul, HPow.hPow, Finset.card, Exists, And, Membership.mem, Prod.mk, HAdd.hAdd and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.