Erdős problem 899
Let be an infinite set such that . Is it true that
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/899.leanTrue ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤SolvedStatement only, no proof