Erdős problem 1082
Let be a set of points with no three on a line. Must there exist a single point from which there are at least distinct distances?
Sources
FormalConjectures/ErdosProblems/
1082.lean
Let be a set of points with no three on a line. Must there exist a single point from which there are at least distinct distances?
This question has been answered negatively by Xichuan in the [comments](https://www.erdosproblems.com/forum/thread/1082), who gave a set of points in , with no three on a line, such that each point determines only distinct distances.
A smaller counterexample has been formalised here: it comprised of points, where each point only determines distances.
This counterexample has originally been found by Heiko Harborth.
False ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.NonTrilinear ↑A → ∃ a, ∃ (_ : a ∈ A), A.card / 2 ≤ EuclideanGeometry.distinctDistancesFrom A a - 1