def SimpleGraph.UnitDistancePlaneGraph (V : Set (EuclideanSpace ℝ (Fin 2))) : SimpleGraph ↑V

A unit distance graph in ℝ²: A graph where the vertices V are a collection of points in ℝ² and there is an edge between two points if and only if the distance between them is 1.

Equations

• SimpleGraph.UnitDistancePlaneGraph V = { Adj := fun (x y : ↑V) => dist x y = 1, symm := ⋯, loopless := ⋯ }