Characterize the realized positive radii
ProvedErdos9796Mission.mem_pinnedRadii_iffdiscrete-geometryerdos-97pinned-distances
A real number r is among the positive radii realized from p in A exactly when r is positive and some point q of A has distance r from p.
Preamble
import Definitions.Def_Erdos9796Mission_PinnedMultiplicity
Formal statement
theorem Erdos9796Mission.mem_pinnedRadii_iff
{A : Finset Erdos9796Mission.Plane} {p : Erdos9796Mission.Plane} {r : ℝ} :
r ∈ Erdos9796Mission.pinnedRadii A p ↔
(∃ q ∈ A, dist p q = r) ∧ 0 < r := by sorrySource