Erdős problem 624
Let be a finite set of size and be such that there is a function so that for every with we have . Prove that .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/624.leanFilter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTopOpenStatement only, no proof