Skip to content

Erdős problem 505

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

505.lean

Retained formal statement3 of 3
FormalConjectures/ErdosProblems/505.leanErdos505.erdos_505.test_dim_one2 linesExact file
∀ (S : Set (EuclideanSpace ℝ (Fin 1))),  Bornology.IsBounded S → 0 < Metric.diam S → ∃ F, S ⊆ ⋃ i, F i ∧ ∀ (i : Fin 2), Metric.diam (F i) < Metric.diam S
TestStatement only, no proof