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

Two-element sets: independent iff mutual non-membership.

A two-element set {x, y} (with x ≠ y) is independent for A if and only if x ∉ A y and y ∉ A x.

FormalConjectures/ErdosProblems/501.leanErdos501.erdos_501.variants.pair_independent_iff1 lineExact file

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

TextbookStatement only, no proof