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
Sattler proved in [Sa75] that the set of odd numbers has property P₁.
Erdos318.P₁ {n | Odd n}SolvedStatement only, no proof