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)