Erdős problem 92
A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is n, since the points equidistant from any x form a subset of the other n - 1 points. This ensures sSup is well-defined.
Sources
FormalConjectures/ErdosProblems/
92.lean
Retained formal statement
A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is n, since the points equidistant from any x form a subset of the other n - 1 points. This ensures sSup is well-defined.
∀ (n : ℕ), BddAbove (Erdos92.possible_f_values n)TestStatement only, no proof