Erdős problem 143 · problems.science

Does this imply that $\liminf \frac{|A \cap [1,x]|}{x} = 0?$

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

143.lean

Retained formal statement1 of 2

Does this imply that $\liminf \frac{|A \cap [1,x]|}{x} = 0?$

FormalConjectures/ErdosProblems/143.leanErdos143.erdos_143.parts.i2 linesExact file

1True ↔2  ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0

OpenStatement only, no proof