Erdős problem 1192
Does there exist, for all , a basis of order (so that for all large ) such that for all ?
Sources
FormalConjectures/ErdosProblems/
1192.lean
Retained formal statement
The empty sum () gives exactly one representation of : the empty tuple.
∀ (A : Set ℕ), Erdos1192.f_r A 0 0 = 1TestStatement only, no proof