Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Face frontiers are unions of whole edges; a cycle edge borders two faces and a bridge borders one
Statement
In a plane graph (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs), if the relative interior of an edge meets the frontier of a face, then the whole edge lies in that frontier. An edge on a cycle is incident with two distinct faces, one on each local side. A bridge is incident with one face on both local sides and is therefore traversed twice in that face's boundary walk. Edge deletion is as in Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, and the bridge cases use the arc-complement fact The complement of a polygonal arc in is polygonally connected.
Facts & Assumptions
Given: A plane graph and an edge .
A polygon has exactly two regions, each with frontier the polygon (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).
An edge is a bridge if and only if it lies on no cycle (An edge of a finite graph is a bridge if and only if it lies on no cycle).
If are disjoint finite unions of plane points and polygonal arcs, and a polygonal arc joins one point of each with its interior inside a region of , then remains a single region of (Diestel, Graph Theory, Lemma 4.1.3, cited above).
Proof
At an interior point of a straight segment of the polygonal arc , a sufficiently small disk meets the drawing only in that segment; its two open sides lie in faces. At each of the finitely many bends, a small disk meets the drawing only in the two adjacent subsegments of , and its two complementary local sides join the corresponding sides of those segments. Overlapping these finitely many local disks along shows that each side stays in the same face throughout the edge interior. Every neighbourhood of an endpoint meets the edge interior, so that endpoint also lies in the frontier of each incident face. Hence any face frontier meeting the edge interior contains the whole edge.
If lies on a cycle , [L1] gives two regions of the polygonal image of . The two local sides of lie in different such regions and cannot be joined in the complement of the full drawing, so they belong to two distinct faces of .
If lies on no cycle, [L2] makes it a bridge. Partition the components of the deleted-edge drawing into two disjoint finite unions of points and arcs , with the endpoints of in different parts. The two local sides lie in one face of that drawing, since a small rectangle across an interior point of joins them there. Apply [F1] to and : is one face of the original drawing. Thus the two local sides border the same face; its boundary walk encounters once on each side.
Depends on
- Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- The complement of a polygonal arc in $\mathbb R^2$ is polygonally connected
- An edge of a finite graph is a bridge if and only if it lies on no cycle
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
Used by
- For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph Corollary
- The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge Definition
- Every edge-maximal graph of order at least four with no subdivision of K₅ or K_3,3 is three-connected Lemma
- Every plane triangulation with at least three vertices is connected Lemma
- Facial boundary walks of a connected plane graph sum to 2|E|, and if every such walk has length at least g then g|F|≤2|E| Lemma
- Finite plane graph ear and face facts Lemma
- If two distinct faces of a connected plane graph have the same boundary subgraph, then the graph is a cycle Lemma
- A two-connected plane graph of order at least three is maximal exactly when every face is triangular Proposition
- Every plane forest has exactly one face Proposition
- Euler's formula |V|-|E|+|F|=2 for every connected plane graph Theorem
- Every connected plane graph has a plane dual multigraph, and when that dual is simple the reciprocal embedding identifies the double dual with the original graph Theorem
Dependency tree · two levels
16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- R. Diestel, Graph Theory, 6th ed., Lemmas 4.1.3 and 4.2.2 (standard reference, not scraped)