Erdős problem 143

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

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