Part 2 of 2

TheoremFive color theorem#●ready to prove

Every straight-line planar simple graph \(G\) on a finite vertex set has a proper vertex coloring with five colors.

theorem_wanted five_color_theorem {V : Type*} [Finite V] (G : SimpleGraph V)
    (hG : G.IsPlanar) :
    Nonempty (G.Coloring (Fin 5))

Sources

• https://en.wikipedia.org/wiki/Five_color_theorem.

Uses 1

Statement usesStraight-line planar graph

TheoremMycielski's theorem#✓fully proved

Write \(\chi(G)\) for the chromatic number of a simple graph \(G\). For every simple graph \(G\) on a finite vertex set there is a simple graph \(H\) on a finite vertex set with strictly more vertices than \(G\) that contains a subgraph isomorphic to \(G\), such that \(H\) is triangle-free whenever \(G\) is, and such that \(\chi(H) = \chi(G) + 1\) whenever \(\chi(G)\) is finite. Moreover, for every natural number \(k\) there is a triangle-free simple graph \(H\) on a finite vertex set with \(\chi(H) \ge k\).

The explicit Mycielski construction is abstracted here to the existence of such a graph \(H\).

theorem mycielski_theorem :
    (∀ (V : Type*) [Fintype V] (G : SimpleGraph V),
      ∃ (W : Type*) (_ : Fintype W) (H : SimpleGraph W),
        G ⊑ H ∧
          Fintype.card V < Fintype.card W ∧
              (G.CliqueFree 3 → H.CliqueFree 3) ∧
                (G.chromaticNumber ≠ ⊤ → H.chromaticNumber = G.chromaticNumber + 1)) ∧
    ∀ (k : ℕ), ∃ (W : Type*) (_ : Fintype W) (H : SimpleGraph W),
      H.CliqueFree 3 ∧ (↑k ≤ H.chromaticNumber)

Sources

• J. Mycielski, "Sur le coloriage des graphes" (1955), https://doi.org/10.4064/cm-3-2-161-162 (statement ID mycielski-theorem-s1).

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.