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

The constant family A x = ∅ satisfies all hypotheses of the main problem: each A x is bounded (the empty set is bounded) and has Lebesgue outer measure 0 < 1. Moreover, all of ℝ is an independent set, showing the conclusion holds trivially.

This demonstrates that the hypotheses are non-vacuous: the family A x = ∅ is a valid input to the theorem, and ℝ (which is infinite) witnesses the conclusion.

FormalConjectures/ErdosProblems/501.leanErdos501.erdos_501.tests.empty_family_is_valid3 linesExact file

1have A := fun x => ∅;2(∀ (x : ℝ), Bornology.IsBounded (A x)) ∧3  (∀ (x : ℝ), MeasureTheory.volume.toOuterMeasure (A x) < 1) ∧ ∃ X, X.Infinite ∧ X.Pairwise fun x y => x ∉ A y

TestStatement only, no proof

Sources

Search problems.science