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 statement4 of 13

The hypothesis volume.toOuterMeasure (A x) < 1 is strictly satisfied when A x = {x} (a singleton), since Lebesgue measure of a singleton is 0.

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

1∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure {x} < 1

TestStatement only, no proof