Skip to content

Erdős problem 92

Start work

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

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

92.lean

Retained formal statement3 of 3

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.

FormalConjectures/ErdosProblems/92.leanErdos92.possible_f_values_BddAbove1 lineExact file
∀ (n : ℕ), BddAbove (Erdos92.possible_f_values n)
TestStatement only, no proof