Erdős problem 501

For every $x \in \mathbb{R}$ let $A_x \subset \mathbb{R}$ be a bounded set of Lebesgue outer measure $< 1$ . Must there be an infinite independent set, that is an infinite $X \subseteq \mathbb{R}$ with $x \notin A_y$ for all distinct $x, y \in X$ ?

Sources

The source's own material, retained exactly.

14 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

501.lean

Retained formal statement6 of 13

The boundary case: the measure condition < 1 is sharp. An interval of length ≥ 1 has Lebesgue measure ≥ 1, so it would fail the hypothesis. Here [0, 1] has measure exactly 1.

FormalConjectures/ErdosProblems/501.leanErdos501.erdos_501.tests.unit_interval_measure1 lineExact file

1MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) = 1

TestStatement only, no proof