Erdős problem 318
There exists a set A with positive density that does not have property P₁. #TODO: prove this lemma by assuming erdos_318.contain_single_even.
Sources
FormalConjectures/ErdosProblems/
318.lean
Retained formal statement
ℕ has property P₁. This is proved in [ErSt75].
Erdos318.P₁ Set.univSolvedStatement only, no proof