Erdős problem 505

Erdős Problem 505 (disproved). Borsuk's conjecture is false for sufficiently large $n$ : there exists a dimension $n$ and a bounded set $S \subseteq \mathbb{R}^n$ with positive diameter such that $S$ cannot be covered by $n + 1$ subsets each of diameter strictly less than $\operatorname{diam}(S)$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

505.lean

Retained formal statement2 of 3

Borsuk's conjecture, small dimensions (open / true for $n \leq 3$ ). Every bounded set $S \subseteq \mathbb{R}^n$ with $n \leq 3$ can be covered by $n + 1$ subsets each of strictly smaller diameter.

Trivial for $n \leq 2$ ; proved for $n = 3$ by Eggleston [Eg55].

FormalConjectures/ErdosProblems/505.leanErdos505.erdos_505.small_dim4 linesExact file

1∀ n ≤ 3,2  ∀ (S : Set (EuclideanSpace ℝ (Fin n))),3    Bornology.IsBounded S →4      0 < Metric.diam S → ∃ F, S ⊆ ⋃ i, F i ∧ ∀ (i : Fin (n + 1)), Metric.diam (F i) < Metric.diam S

SolvedStatement only, no proof