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.pathGraph n).Coloring 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).Embedding (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 = { toFun := fun (v : Fin 2) => ⟨↑v, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

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