Erdős problem 955
If has density then must also have density .
Sources
FormalConjectures/ErdosProblems/
955.lean
Retained formal statement
If has density then must also have density .
A conjecture of Erdős, Granville, Pomerance, and Spiro [EGPS90].
True ↔ ∀ (A : Set ℕ), A.HasDensity 0 → {x | Erdos955.s x ∈ A}.HasDensity 0OpenStatement only, no proof