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 .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/505.lean∃ n S, Bornology.IsBounded S ∧ 0 < Metric.diam S ∧ ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:505 - PLBY Lean proofs
ErdosProblems.Erdos505
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine