Borsuk's conjecture

DefinitionBorsuk covers#✓fully proved

Let \(s\) be a set in an extended pseudometric space and let \(k\) be a natural number. The set \(s\) has a \(k\)-piece Borsuk cover if there are \(k\) sets whose union contains \(s\), each of extended diameter strictly smaller than that of \(s\).

def HasBorsukCover {E : Type*} [PseudoEMetricSpace E] (k : ℕ) (s : Set E) : Prop :=
  ∃ c : Fin k → Set E, s ⊆ ⋃ i, c i ∧ ∀ i, ediam (c i) < ediam s

Used by 8

Used byUpper bounds on the Borsuk number of a Euclidean space · Borsuk covers by closed sets · Borsuk covers by subsets · Enlarging a Borsuk cover · Borsuk covers of nonempty sets have at least one piece · Borsuk number of a set · Bounds on the Borsuk number of a set · A Borsuk cover bounds the Borsuk number

DefinitionBorsuk number of a set#✓fully proved

The Borsuk number of a set \(s\) in the Euclidean space \(\mathbb{R}^n\) is the least natural number \(k\) such that \(s\) has a \(k\)-piece Borsuk cover, that is, \(s\) is covered by \(k\) sets each of strictly smaller extended diameter than \(s\); it is \(\infty\) if no such \(k\) exists.

noncomputable def setBorsukNumber {n : ℕ} (s : Set (EuclideanSpace ℝ (Fin n))) : ℕ∞ :=
  ⨅ k : {k : ℕ // HasBorsukCover k s}, (k.val : ℕ∞)

Uses 1 · Used by 5

Statement usesBorsuk covers

Used byBorsuk number of a Euclidean space · Upper bounds on the Borsuk number of a Euclidean space · Bounds on the Borsuk number of a set · A Borsuk cover bounds the Borsuk number · Two-distance Borsuk number in dimension \(n\)

DefinitionBorsuk number of a Euclidean space#✓fully proved

For a natural number \(n\), the Borsuk number of the Euclidean space \(\mathbb{R}^n\) is the supremum, in \(\mathbb{N} \cup \{\infty\}\), of the Borsuk numbers of the bounded subsets of \(\mathbb{R}^n\) with at least two points.

noncomputable def dimensionBorsukNumber (n : ℕ) : ℕ∞ :=
  ⨆ s : {s : Set (EuclideanSpace ℝ (Fin n)) // IsBounded s ∧ s.Nontrivial},
    setBorsukNumber s.val

Uses 1 · Used by 4

Statement usesBorsuk number of a set

Used byBorsuk's conjecture in a given dimension · Upper bounds on the Borsuk number of a Euclidean space · First Borsuk failure dimension · When the first Borsuk failure dimension is infinite

DefinitionFirst Borsuk failure dimension#✓fully proved

The first Borsuk failure dimension is the least positive integer \(n\) such that the Borsuk number of the Euclidean space \(\mathbb{R}^n\) is greater than \(n + 1\), and \(\infty\) if there is no such \(n\).

noncomputable def firstBorsukFailureDimension : ℕ∞ :=
  ⨅ n : {n : ℕ // 0 < n ∧ (n + 1 : ℕ∞) < dimensionBorsukNumber n}, (n.val : ℕ∞)

Uses 1 · Used by 1

Statement usesBorsuk number of a Euclidean space

Used byWhen the first Borsuk failure dimension is infinite

TheoremA Borsuk cover bounds the Borsuk number#✓fully proved

If a set \(s\) in the Euclidean space \(\mathbb{R}^n\) has a \(k\)-piece Borsuk cover for a natural number \(k\), then the Borsuk number of \(s\) is at most \(k\).

theorem setBorsukNumber_le_of_cover {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    (h : HasBorsukCover k s) : setBorsukNumber s ≤ k

Uses 2 · Used by 2

Statement usesBorsuk covers · Borsuk number of a set

Used byUpper bounds on the Borsuk number of a Euclidean space · Bounds on the Borsuk number of a set

TheoremBorsuk covers by subsets#✓fully proved

For natural numbers \(n\) and \(k\), a set \(s\) in the Euclidean space \(\mathbb{R}^n\) has a \(k\)-piece Borsuk cover if and only if there are subsets \(c_1, \dots, c_k\) of \(s\) with \(s = c_1 \cup \dots \cup c_k\), each of extended diameter strictly smaller than that of \(s\).

theorem hasBorsukCover_iff_exactUnion {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))} :
    HasBorsukCover k s ↔ ∃ c : Fin k → Set (EuclideanSpace ℝ (Fin n)),
      (∀ i, c i ⊆ s) ∧ s = ⋃ i, c i ∧ ∀ i, ediam (c i) < ediam s

Uses 1

Statement usesBorsuk covers

TheoremBorsuk covers by closed sets#✓fully proved

For natural numbers \(n\) and \(k\), a set \(s\) in the Euclidean space \(\mathbb{R}^n\) has a \(k\)-piece Borsuk cover if and only if there are \(k\) closed subsets of \(\mathbb{R}^n\) whose union contains \(s\), each of extended diameter strictly smaller than that of \(s\).

theorem hasBorsukCover_iff_closedCover {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))} :
    HasBorsukCover k s ↔ ∃ c : Fin k → Set (EuclideanSpace ℝ (Fin n)),
      s ⊆ ⋃ i, c i ∧ ∀ i, IsClosed (c i) ∧ ediam (c i) < ediam s

Uses 1

Statement usesBorsuk covers

TheoremBorsuk covers of nonempty sets have at least one piece#✓fully proved

Let \(n\) and \(k\) be natural numbers. If a nonempty set \(s\) in the Euclidean space \(\mathbb{R}^n\) has a \(k\)-piece Borsuk cover, then \(0 < k\).

theorem hasBorsukCover_pos {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    (hs : s.Nonempty) (h : HasBorsukCover k s) : 0 < k

Uses 1 · Used by 1

Statement usesBorsuk covers

Used byEnlarging a Borsuk cover

TheoremEnlarging a Borsuk cover#✓fully proved

Let \(n\), \(k\) and \(l\) be natural numbers with \(k \le l\). If a nonempty set \(s\) in the Euclidean space \(\mathbb{R}^n\) has a \(k\)-piece Borsuk cover, then \(s\) has an \(l\)-piece Borsuk cover.

Repeating an existing piece enlarges the cover to the larger size.

theorem hasBorsukCover_mono {n k l : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    (hs : s.Nonempty) (h : HasBorsukCover k s) (hkl : k ≤ l) : HasBorsukCover l s

Uses 2 · Used by 1

Statement usesBorsuk covers

Proof usesBorsuk covers of nonempty sets have at least one piece

Used byBounds on the Borsuk number of a set

TheoremBounds on the Borsuk number of a set#✓fully proved

For a nonempty set \(s\) in the Euclidean space \(\mathbb{R}^n\) and a natural number \(k\), the Borsuk number of \(s\) is at most \(k\) if and only if \(s\) has a \(k\)-piece Borsuk cover.

theorem setBorsukNumber_le_iff {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    (hs : s.Nonempty) : setBorsukNumber s ≤ k ↔ HasBorsukCover k s

Uses 4 · Used by 1

Statement usesBorsuk covers · Borsuk number of a set

Proof usesEnlarging a Borsuk cover · A Borsuk cover bounds the Borsuk number

Used byUpper bounds on the Borsuk number of a Euclidean space

TheoremUpper bounds on the Borsuk number of a Euclidean space#✓fully proved

For natural numbers \(n\) and \(k\), the Borsuk number of the Euclidean space \(\mathbb{R}^n\) is at most \(k\) if and only if every bounded subset \(s\) of \(\mathbb{R}^n\) with at least two points has a \(k\)-piece Borsuk cover, that is, \(s\) is covered by \(k\) sets, each of extended diameter strictly smaller than that of \(s\).

theorem dimensionBorsukNumber_le_iff {n k : ℕ} : dimensionBorsukNumber n ≤ k ↔
    ∀ s : Set (EuclideanSpace ℝ (Fin n)),
      IsBounded s → s.Nontrivial → HasBorsukCover k s

Uses 5

Statement usesBorsuk covers · Borsuk number of a Euclidean space

Proof usesBorsuk number of a set · Bounds on the Borsuk number of a set · A Borsuk cover bounds the Borsuk number

DefinitionBorsuk's conjecture in a given dimension#✓fully proved

For a natural number \(n\), Borsuk's conjecture in dimension \(n\) is the statement that the Borsuk number of the Euclidean space \(\mathbb{R}^n\) is at most \(n + 1\).

Equivalently, every bounded subset of \(\mathbb{R}^n\) with at least two points is covered by \(n + 1\) sets, each of extended diameter strictly smaller than that of the set.

def borsukConjectureInDimension (n : ℕ) : Prop := dimensionBorsukNumber n ≤ (n + 1 : ℕ∞)

Uses 1

Statement usesBorsuk number of a Euclidean space

TheoremWhen the first Borsuk failure dimension is infinite#✓fully proved

The first Borsuk failure dimension is \(\infty\) if and only if, for every positive integer \(n\), the Borsuk number of the Euclidean space \(\mathbb{R}^n\) is at most \(n + 1\).

theorem firstBorsukFailureDimension_eq_top_iff : firstBorsukFailureDimension = ⊤ ↔
    ∀ n : ℕ, 0 < n → dimensionBorsukNumber n ≤ (n + 1 : ℕ∞)

Uses 2

Statement usesBorsuk number of a Euclidean space · First Borsuk failure dimension

DefinitionTwo-distance sets#✓fully proved

A set \(s\) in the Euclidean space \(\mathbb{R}^n\) is a two-distance set if there are reals \(0 < a < b\) such that the distance between any two distinct points of \(s\) is \(a\) or \(b\), and both \(a\) and \(b\) occur as the distance between some two points of \(s\).

def IsTwoDistanceSet {n : ℕ} (s : Set (EuclideanSpace ℝ (Fin n))) : Prop :=
  ∃ a b : ℝ, 0 < a ∧ a < b ∧
    (∀ x ∈ s, ∀ y ∈ s, x ≠ y → dist x y = a ∨ dist x y = b) ∧
    (∃ x ∈ s, ∃ y ∈ s, dist x y = a) ∧
    ∃ x ∈ s, ∃ y ∈ s, dist x y = b

Used by 1

Used byTwo-distance Borsuk number in dimension \(n\)

DefinitionTwo-distance Borsuk number in dimension \(n\)#✓fully proved

The two-distance Borsuk number in dimension \(n\) is the supremum, taken in \(\mathbb{N} \cup \{\infty\}\), of the Borsuk numbers of all bounded two-distance sets with at least two points in the Euclidean space \(\mathbb{R}^n\).

noncomputable def twoDistanceBorsukNumber (n : ℕ) : ℕ∞ :=
  ⨆ s : {s : Set (EuclideanSpace ℝ (Fin n)) //
      Bornology.IsBounded s ∧ s.Nontrivial ∧ IsTwoDistanceSet s}, setBorsukNumber s.val

Uses 2

Statement usesTwo-distance sets · Borsuk number of a set

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.