Erdős problem 99
For sufficiently large n, is it the case that any set of n points with minimum distance that minimizes diameter must contain an equilateral triangle of side length 1?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/99.leanTrue ↔ ∀ᶠ (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 rOpenStatement only, no proof