Skip to content

Erdős problem 99

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

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 11 that minimizes diameter must contain an equilateral triangle of side length 1?

FormalConjectures/ErdosProblems/99.leanErdos99.erdos_997 linesExact file
True ↔  ∀ᶠ (n : ℕ) in Filter.atTop,    ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))),      A.card = n →        Erdos99.HasMinDist1 A →          IsMinOn (fun B => Metric.diam ↑B) {B | B.card = n ∧ Erdos99.HasMinDist1 B} A →            ∃ p ∈ A, ∃ q ∈ A, ∃ r ∈ A, Erdos99.FormsEquilateralTriangle p q r
OpenStatement only, no proof