Erdős problem 96 · problems.science

This lemma confirms that the set of possible unit-distance counts is bounded above, which ensures that taking the supremum (sSup) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$ .

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

96.lean

Retained formal statement2 of 2

If $n$ points in $\mathbb{R}^2$ form a convex polygon then there are $O(n)$ many pairs which are distance $1$ apart.

FormalConjectures/ErdosProblems/96.leanErdos96.erdos_961 lineExact file

1True ↔ (fun n => ↑(Erdos96.maxConvexUnitDistances n)) =O[Filter.atTop] fun n => ↑n

OpenStatement only, no proof

Sources

Search problems.science