Concrete colorings of common graphs

This file defines colorings for some common graphs

Main declarations

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

theorem SimpleGraph.two_le_chromaticNumber_of_adj {α : Type u_1} {G : SimpleGraph α} {u v : α} (hAdj : G.Adj u v) : 2 ≤ G.chromaticNumber

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

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