Erdős problem 12
Let be infinite with no distinct such that with . Can have positive lower limit? Must every such fall below infinitely often?
Sources
FormalConjectures/ErdosProblems/
12.lean
Retained formal statement
Let be an infinite set such that there are no distinct such that and . Is it true that ?
sorry ↔ ∀ (A : Set ℕ), Erdos12.IsGood A → Summable fun n => 1 / ↑↑nOpenStatement only, no proof