noncomputable def unitDistNum {X : Type u_1} [MetricSpace X] (s : Finset X) : ℕ

The number of pairs of points of a finite set s in a metric space that are distance 1 apart.

Equations

• unitDistNum s = {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}.card