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
Hechler (1972) [He72]: the answer to the main question is NO, assuming the continuum hypothesis.
Assuming CH (ℵ₁ = 𝔠), there exists a family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1 for which no infinite independent set exists.
True ↔ Cardinal.aleph 1 = Cardinal.continuum → ∃ A, (∀ (x : ℝ), Bornology.IsBounded (A x)) ∧ (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) ∧ ¬∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A ySolvedStatement only, no proof