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

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

318.lean

Retained formal statement4 of 7

Every infinite arithmetic progression has property P₁. This is proved in [Sa82b].

FormalConjectures/ErdosProblems/318.leanErdos318.erdos_318.variants.infinite_AP1 lineExact file

1∀ {A : Set ℕ}, A.IsAPOfLength ⊤ → Erdos318.P₁ A

SolvedStatement only, no proof