Erdős problem 99 · problems.science

For sufficiently large n, is it the case that any set of n points with minimum distance $1$ that minimizes diameter must contain an equilateral triangle of side length 1?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

99.lean

Retained formal statement1 of 1

For sufficiently large n, is it the case that any set of n points with minimum distance $1$ that minimizes diameter must contain an equilateral triangle of side length 1?

FormalConjectures/ErdosProblems/99.leanErdos99.erdos_997 linesExact file

1True ↔2  ∀ᶠ (n : ℕ) in Filter.atTop,3    ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),4      A.card = n →5        Erdos99.HasMinDist1 A →6          IsMinOn (fun B => Metric.diam ↑B) {B | B.card = n ∧ Erdos99.HasMinDist1 B} A →7            ∃ p ∈ A, ∃ q ∈ A, ∃ r ∈ A, Erdos99.FormsEquilateralTriangle p q r

OpenStatement only, no proof

Sources

Search problems.science