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
Gladysz (1962) [Gl62]: independent set of size 2 in the closed case.
If all the sets A x are closed with Lebesgue measure < 1, then there exist two distinct reals x y such that x ∉ A y and y ∉ A x.
This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski– Seredyński theorem [NPS87].
True ↔ ∀ (A : ℝ → Set ℝ), (∀ (x : ℝ), IsClosed (A x)) → (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ X, 2 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A ySolvedStatement only, no proof