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.

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.

The density sits in an existential, so HasPosDensity is the *stronger* reading here and weakening it to positive lower density would claim less, which is the opposite of the usual situation for Erdős' "positive density". It also costs nothing: by erdos_318.variants.contain_single_even a witness only needs exactly one even element, and the odd numbers together with one even number have density 1 / 2 on the nose.