Erdős problem 318 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

318.lean

Retained formal statement3 of 7

For any set A containing exactly one even number, A does not have property P₁. Sattler [Sa82] credits this observation to Erdős, who presumably found this after [ErGr80].

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

1∀ {A : Set ℕ}, {n | n ∈ A ∧ Even n}.ncard = 1 → ¬Erdos318.P₁ A

SolvedStatement only, no proof

Sources

Search problems.science