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
Closed sets case: existence of an independent set of size 3.
If the sets A x are closed with Lebesgue measure < 1, must there exist an independent set of size 3?
This is implied by the stronger theorem of Newelski–Pawlikowski–Seredyński [NPS87] below; Gladysz [Gl62] earlier proved the existence of an independent set of size 2.
True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ X, 3 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A ySolvedStatement only, no proof