Problem 97 holds through nine points
ProvedErdos9796Mission.not_hasNEquidistantProperty_four_of_card_le_ninediscrete-geometryerdos-97small-cardinality
Every nonempty finite planar point set of at most nine points in strictly convex position has a vertex for which no positive-radius circle centered there contains four other points of the set.
Preamble
import Theorems.Thm_Erdos9796Mission_counterexample_card_ge_nine import Theorems.Thm_Erdos9796Mission_finite_nine_exclusion open Erdos9796Mission
Formal statement
theorem Erdos9796Mission.not_hasNEquidistantProperty_four_of_card_le_nine :
∀ A : Finset Plane, A.Nonempty → ConvexIndep (A : Set Plane) →
A.card ≤ 9 → ¬ HasNEquidistantProperty 4 A := by sorrySource