Erdős Problem 982

Reference: erdosproblems.com/982

theorem Erdos982.erdos_982 (n : ℕ) (hn : 3 ≤ n) (p : Fin n → EuclideanSpace ℝ (Fin 2)) (hp : Function.Injective p) (hp' : EuclideanGeometry.IsConvexPolygon p) : ∃ (i : Fin n), {d : ℝ | ∃ (j : Fin n), j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then some vertex has at least $\lfloor\frac{n}{2}\rfloor$ different distances to other vertices.