Skip to content

Erdős problem 501

For every x∈Rx \in \mathbb{R} let Ax⊂RA_x \subset \mathbb{R} be a bounded set of Lebesgue outer measure <1< 1. Must there be an infinite independent set, that is an infinite X⊆RX \subseteq \mathbb{R} with x∉Ayx \notin A_y for all distinct x,y∈Xx, y \in X?

Sources

The source's own material, retained exactly.

14 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

501.lean

Retained formal statement9 of 13

Gladysz (1962) [Gl62]: independent set of size 2 in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there exist two distinct reals x y such that x ∉ A y and y ∉ A x.

This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski– Seredyński theorem [NPS87].

FormalConjectures/ErdosProblems/501.leanErdos501.erdos_501.variants.gladysz_size24 linesExact file
True ↔  ∀ (A : ℝ → Set ℝ),    (∀ (x : ℝ), IsClosed (A x)) →      (∀ (x : ℝ), MeasureTheory.volume (A x) < 1) → ∃ X, 2 ≤ X.ncard ∧ X.Pairwise fun x y => x ∉ A y
SolvedStatement only, no proof