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
The boundary case: the measure condition < 1 is sharp. An interval of length ≥ 1 has Lebesgue measure ≥ 1, so it would fail the hypothesis. Here [0, 1] has measure exactly 1.
MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) = 1TestStatement only, no proof