Erdős problem 505
Erdős Problem 505 (disproved). Borsuk's conjecture is false for sufficiently large : there exists a dimension and a bounded set with positive diameter such that cannot be covered by subsets each of diameter strictly less than .
Sources
FormalConjectures/ErdosProblems/
505.lean
Retained formal statement
∀ (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 STestStatement only, no proof