Documentation

Mathlib.Combinatorics.SimpleGraph.ConcreteColorings

Concrete colorings of common graphs #

This file defines colorings for some common graphs

Main declarations #

theorem SimpleGraph.two_le_chromaticNumber_of_adj {α : Type u_1} {G : SimpleGraph α} {u v : α} (hadj : G.Adj u v) :

Bicoloring of a path graph

Equations
Instances For

    Embedding of pathGraph 2 into the first two elements of pathGraph n for 2 ≤ n

    Equations
    Instances For
      theorem SimpleGraph.Coloring.even_length_iff_congr {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
      Even p.length (c u = true c v = true)
      theorem SimpleGraph.Coloring.odd_length_iff_not_congr {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
      Odd p.length (¬c u = true c v = true)
      theorem SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop {α : Type u_1} {G : SimpleGraph α} {u : α} (p : G.Walk u u) (hOdd : Odd p.length) :

      Bicoloring of a cycle graph of even size

      Equations
      Instances For

        Tricoloring of a cycle graph

        Equations
        Instances For

          The injection (x₁, x₂) ↦ x₁ is always a r-coloring of a completeEquipartiteGraph r ·.

          Equations
          Instances For
            theorem SimpleGraph.two_colorable_iff_forall_loop_even {α : Type u_1} {G : SimpleGraph α} :
            G.Colorable 2 ∀ (u : α) (w : G.Walk u u), Even w.length