Erdős problem 100

From [Piepmeyer]: 9 points with diameter $< 5$ . TODO: find reference

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

100.lean

Retained formal statement5 of 5

Stronger conjecture: diameter $\geq n - 1$ for sufficiently large $n$ .

FormalConjectures/ErdosProblems/100.leanErdos100.erdos_100.variants.strong2 linesExact file

1∀ᶠ (n : ℕ) in Filter.atTop,2  ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A ≥ ↑n - 1

OpenStatement only, no proof