The repeated-distance property is a pointwise multiplicity bound
ProvedErdos9796Mission.hasNEquidistantProperty_iff_forall_le_pinnedMultiplicitydiscrete-geometryerdos-97pinned-distances
For n > 0, the repeated-distance property gives pinned multiplicity at least n at every point of A, and those pointwise bounds give the repeated-distance property.
Preamble
import Definitions.Def_Erdos9796Mission_PinnedMultiplicity
Formal statement
theorem Erdos9796Mission.hasNEquidistantProperty_iff_forall_le_pinnedMultiplicity
{A : Finset Erdos9796Mission.Plane} {n : ℕ} (hn : 0 < n) :
Erdos9796Mission.HasNEquidistantProperty n A ↔
∀ p ∈ A, n ≤ Erdos9796Mission.pinnedMultiplicity A p := by sorrySource