Documentation

Mathlib.Combinatorics.SimpleGraph.ConcreteColorings

Concrete colorings of common graphs #

This file defines colorings for some common graphs

Main declarations #

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.chromaticNumber_pathGraph (n : ) (h : 2 n) :
      (SimpleGraph.pathGraph n).chromaticNumber = 2
      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) :
      3 G.chromaticNumber