Skip to content

Erdős problem 501

Start work

For every x∈Rx \in \mathbb{R} let Ax⊂RA_x \subset \mathbb{R} be a bounded set of Lebesgue outer measure <1< 1. Must there be an infinite independent set, that is an infinite X⊆RX \subseteq \mathbb{R} with x∉Ayx \notin A_y for all distinct x,y∈Xx, y \in X?

Sources

The source's own material, retained exactly.

14 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

501.lean

Retained formal statement10 of 13

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.

FormalConjectures/ErdosProblems/501.leanErdos501.erdos_501.variants.hechler_CH5 linesExact file
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 y
SolvedStatement only, no proof