Erdős problem 120
Let be an infinite set. Must there be a set of positive measure which does not contain any set of the shape for some and ?
Sources
FormalConjectures/ErdosProblems/
120.lean
Retained formal statement
Let be an infinite set. Must there be a set of positive measure which does not contain any set of the shape for some and ?
True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For AOpenStatement only, no proof