Erdős problem 96
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, .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/96.lean∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)TestStatement only, no proof