Polygonal drawings of arbitrary declared point sets

Sparse and repeated declarations of isolated vertices need no extra darts or routes. Distinct declared names have distinct real-axis positions. This includes the empty graph.

def Cslib.Complexity.Graph.PolygonalDrawing.points (vertices : List ℕ) : { vertices := vertices, edges := [] }.PolygonalDrawing

Draw an arbitrary list of declared isolates at their natural-number real-axis positions. Repeated occurrences of a name retain the same point.

theorem Cslib.Complexity.Graph.PolygonalDrawing.points_isEmbedding (vertices : List ℕ) : (points vertices).IsEmbedding

All distinct declared isolates are separated, independently of sparsity or repetition.

theorem Cslib.Complexity.Graph.PolygonalDrawing.points_realizes (vertices : List ℕ) (r : { vertices := vertices, edges := [] }.RotationSystem) : (points vertices).Realizes r

Every rotation of an edgeless listed graph is realized by its declared point drawing.