Erdős problem 158
Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/158.lean∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon AAPIStatement only, no proof