Concrete colorings of common graphs

This file defines colorings for some common graphs

Main declarations

• SimpleGraph.pathGraph.bicoloring: Bicoloring of a path graph.

def SimpleGraph.pathGraph.bicoloring (n : ℕ) : SimpleGraph.Coloring (SimpleGraph.pathGraph n) Bool

Bicoloring of a path graph

Equations

• SimpleGraph.pathGraph.bicoloring n = SimpleGraph.Coloring.mk (fun (u : Fin n) => decide (↑u % 2 = 0)) ⋯

def SimpleGraph.pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : SimpleGraph.pathGraph 2 ↪g SimpleGraph.pathGraph n

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

Equations

• SimpleGraph.pathGraph_two_embedding n h = { toEmbedding := { toFun := fun (v : Fin 2) => { val := ↑v, isLt := ⋯ }, inj' := ⋯ }, map_rel_iff' := ⋯ }

theorem SimpleGraph.chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) : SimpleGraph.chromaticNumber (SimpleGraph.pathGraph n) = 2