Erdős problem 100
From [Piepmeyer]: 9 points with diameter . TODO: find reference
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/100.leanTrue ↔ ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑nOpenStatement only, no proof