The Königsberg bridges problem #
We show that a graph that represents the islands and mainlands of Königsberg and seven bridges between them has no Eulerian trail.
- V1: Konigsberg.Verts
- V2: Konigsberg.Verts
- V3: Konigsberg.Verts
- V4: Konigsberg.Verts
- B1: Konigsberg.Verts
- B2: Konigsberg.Verts
- B3: Konigsberg.Verts
- B4: Konigsberg.Verts
- B5: Konigsberg.Verts
- B6: Konigsberg.Verts
- B7: Konigsberg.Verts
The vertices for the Königsberg graph; four vertices for the bodies of land and seven vertices for the bridges.
Instances For
Each of the connections between the islands/mainlands and the bridges.
These are ordered pairs, but the data becomes symmetric in Konigsberg.adj
.
Instances For
The adjacency relation for the Königsberg graph.
Instances For
The Königsberg graph structure. While the Königsberg bridge problem is usually described using a multigraph, the we use a "mediant" construction to transform it into a simple graph -- every edge in the multigraph is subdivided into a path of two edges. This construction preserves whether a graph is Eulerian.
(TODO: once mathlib has multigraphs, either prove the mediant construction preserves the Eulerian property or switch this file to use multigraphs.
Instances For
To speed up the proof, this is a cache of all the degrees of each vertex,
proved in Konigsberg.degree_eq_degree
.
Instances For
The Königsberg graph is not Eulerian.