Every counterexample has at least ten points
ProvedErdos9796Mission.counterexample_card_ge_tendiscrete-geometryerdos-97small-cardinality
Every nonempty finite planar point set in strictly convex position such that, at each vertex, four other points lie at some common positive distance from that vertex has at least ten points. The radius may depend on the vertex.
Preamble
import Theorems.Thm_Erdos9796Mission_counterexample_card_ge_nine import Theorems.Thm_Erdos9796Mission_finite_nine_exclusion open Erdos9796Mission
Formal statement
theorem Erdos9796Mission.counterexample_card_ge_ten :
∀ A : Finset Plane, A.Nonempty → ConvexIndep (A : Set Plane) →
HasNEquidistantProperty 4 A → 10 ≤ A.card := by sorrySource