Erdős problem 501
For every let be a bounded set of Lebesgue outer measure . Must there be an infinite independent set, that is an infinite with for all distinct ?
Sources
FormalConjectures/ErdosProblems/
501.lean
Retained formal statement
Newelski–Pawlikowski–Seredyński (1987) [NPS87]: infinite independent set in the closed case.
If all the sets A x are closed with Lebesgue measure < 1, then there is an infinite independent set. This gives a strong affirmative answer to the second question of Problem 501.
True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A ySolvedStatement only, no proof