Erdős problem 501 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

14 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

501.lean

Retained formal statement5 of 13

A singleton {0} is an independent set for any family A : ℝ → Set ℝ, as witnessed by erdos_501.variants.singleton_independent.

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

1∀ (A : ℝ → Set ℝ), {0}.Pairwise fun x y => x ∉ A y

TestStatement only, no proof

Sources

Search problems.science