Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs

A plane graph is a finite simple graph (A finite simple graph is a finite vertex set together with a set of two-element vertex subsets) together with distinct points of $\mathbb R^2$ for its vertices and a polygonal arc (Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in $\mathbb R^2$) for each edge, joining its endpoints, such that an edge interior contains no vertex and two edge arcs meet only at a common endpoint. A finite simple graph is planar if it is isomorphic to the abstract graph underlying some plane graph.

A face is a region of the complement of the drawing (Regions of the complement of a planar set and their frontiers). The boundary subgraph of a face consists of the vertices and whole edges lying in its frontier; this is a subgraph in the sense of Subgraphs, induced subgraphs and spanning subgraphs.

For a connected plane graph, walking once around a face with that face locally on the same side gives its facial boundary walk. Its length is the number of edge traversals, not the number of distinct edges: an edge incident with the same face on both local sides is traversed twice. For a disconnected plane graph a face may have several boundary walks; its boundary length is the sum of their lengths. No boundary walk is assumed to be a cycle unless a later connectivity result proves it.