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.

source
@[protected, instance]
def konigsberg.verts.fintype  :
fintype konigsberg.verts
source
@[protected, instance]
def konigsberg.verts.decidable_eq  :
decidable_eq konigsberg.verts
source
@[nolint]
inductive konigsberg.verts  :
Type

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

Instances for konigsberg.verts
source
def konigsberg.edges  :
list (konigsberg.verts × konigsberg.verts)

Each of the connections between the islands/mainlands and the bridges. These are ordered pairs, but the data becomes symmetric in konigsberg.adj.

Equations
source
def konigsberg.adj (v w : konigsberg.verts) :
bool

The adjacency relation for the Königsberg graph.

Equations
source
def konigsberg.graph  :
simple_graph konigsberg.verts

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.

Equations
source
@[simp]
theorem konigsberg.graph_adj (v w : konigsberg.verts) :
konigsberg.graph.adj v w = ↥(konigsberg.adj v w)
source
@[protected, instance]
def konigsberg.adj.decidable_rel  :
decidable_rel konigsberg.graph.adj
Equations
source
@[simp]
def konigsberg.degree  :
konigsberg.verts → ℕ

To speed up the proof, this is a cache of all the degrees of each vertex, proved in konigsberg.degree_eq_degree.

Equations
source
@[simp]
theorem konigsberg.degree_eq_degree (v : konigsberg.verts) :
konigsberg.graph.degree v = konigsberg.degree v
source
theorem konigsberg.not_is_eulerian {u v : konigsberg.verts} (p : konigsberg.graph.walk u v) (h : p.is_eulerian) :
false

The Königsberg graph is not Eulerian.