Erdős problem 982
If distinct points in form a convex polygon then some vertex has at least different distances to other vertices.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/982.lean∀ (n : ℕ), 3 ≤ n → ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)), Function.Injective p → EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2OpenStatement only, no proof