Skip to content

Erdős problem 318

Start work

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

Open selected source

FormalConjectures/ErdosProblems/

318.lean

Retained formal statement7 of 7

ℕ has property P₁. This is proved in [ErSt75].

FormalConjectures/ErdosProblems/318.leanErdos318.erdos_318.variants.univ1 lineExact file
Erdos318.P₁ Set.univ
SolvedStatement only, no proof