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
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.
∀ (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