mathlib3 documentation

mathlib-archive / wiedijk_100_theorems.konigsberg

The Königsberg bridges problem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We show that a graph that represents the islands and mainlands of Königsberg and seven bridges between them has no Eulerian trail.

@[protected, instance]
inductive konigsberg.verts  :

The vertices for the Königsberg graph; four vertices for the bodies of land and seven vertices for the bridges.

Instances for konigsberg.verts

The adjacency relation for the Königsberg graph.


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.


The Königsberg graph is not Eulerian.