Skip to content

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, (n2)\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 statement1 of 2

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, (n2)\binom{n}{2}.

FormalConjectures/ErdosProblems/96.leanErdos96.convexUnitDistanceCounts_bddAbove1 lineExact file
∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)
TestStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page