Erdős problem 982 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

982.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/982.leanErdos982.erdos_9825 linesExact file

1∀ (n : ℕ),2  3 ≤ n →3    ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)),4      Function.Injective p →5        EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

OpenStatement only, no proof

Sources

Search problems.science