Erdős problem 501
For every let be a bounded set of Lebesgue outer measure . Must there be an infinite independent set, that is an infinite with for all distinct ?
Sources
FormalConjectures/ErdosProblems/
501.lean
Retained formal statement
Trivial lower bound: a single-element set is always independent.
For any family A, any singleton {x} is vacuously independent: there are no two distinct elements.
∀ (A : ℝ → Set ℝ) (x : ℝ), {x}.Pairwise fun x y => x ∉ A yTextbookStatement only, no proof