Documentation

Archive.Wiedijk100Theorems.Konigsberg

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.

source
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
    source
    instance Konigsberg.instDecidableEqVerts :
    DecidableEq Konigsberg.Verts
    source
    instance Konigsberg.instFintypeVerts :
    Fintype 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.

    Instances For
      source
      def Konigsberg.adj (v : Konigsberg.Verts) (w : Konigsberg.Verts) :
      Bool

      The adjacency relation for the Königsberg graph.

      Instances For
        source
        @[simp]
        theorem Konigsberg.graph_Adj (v : Konigsberg.Verts) (w : Konigsberg.Verts) :
        SimpleGraph.Adj Konigsberg.graph v w = (Konigsberg.adj v w = true)
        source
        def Konigsberg.graph :
        SimpleGraph 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.

        Instances For
          source
          instance Konigsberg.instDecidableRelVertsAdjGraph :
          DecidableRel Konigsberg.graph.Adj
          source
          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.

          Instances For
            source
            @[simp]
            theorem Konigsberg.degree_eq_degree (v : Konigsberg.Verts) :
            SimpleGraph.degree Konigsberg.graph v = Konigsberg.degree v
            source
            theorem Konigsberg.not_even_degree_iff (w : Konigsberg.Verts) :
            ¬Even (Konigsberg.degree w) ↔ w = Konigsberg.Verts.V1 ∨ w = Konigsberg.Verts.V2 ∨ w = Konigsberg.Verts.V3 ∨ w = Konigsberg.Verts.V4
            source
            theorem Konigsberg.setOf_odd_degree_eq :
            {v | Odd (SimpleGraph.degree Konigsberg.graph v)} = {Konigsberg.Verts.V1, Konigsberg.Verts.V2, Konigsberg.Verts.V3, Konigsberg.Verts.V4}
            source
            theorem Konigsberg.not_isEulerian {u : Konigsberg.Verts} {v : Konigsberg.Verts} (p : SimpleGraph.Walk Konigsberg.graph u v) (h : SimpleGraph.Walk.IsEulerian p) :
            False

            The Königsberg graph is not Eulerian.