theorem SimpleGraph.le_chromaticNumber_iff_colorable {V : Type u_1} {G : SimpleGraph V} {n : ℕ} : ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ), G.Colorable m → n ≤ m

theorem SimpleGraph.le_chromaticNumber_iff_coloring {V : Type u_1} {G : SimpleGraph V} {n : ℕ} : ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ) (a : G.Coloring (Fin m)), n ≤ m

theorem SimpleGraph.Coloring.injective_comp_of_pairwise_adj {V : Type u_1} {α : Type u_2} {ι : Type u_3} {G : SimpleGraph V} (C : G.Coloring α) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : Function.Injective (⇑C ∘ f)

theorem SimpleGraph.Colorable.card_le_of_pairwise_adj {V : Type u_1} {ι : Type u_3} {G : SimpleGraph V} {n : ℕ} (hG : G.Colorable n) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : Nat.card ι ≤ n

theorem SimpleGraph.le_chromaticNumber_of_pairwise_adj {V : Type u_1} {ι : Type u_3} {G : SimpleGraph V} {n : ℕ} (hn : n ≤ Nat.card ι) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : ↑n ≤ G.chromaticNumber

instance SimpleGraph.instIsSymmAdj_formalConjecturesForMathlib {V : Type u_1} {ι : Type u_3} {G : SimpleGraph V} (f : ι → V) : IsSymm ι fun (i j : ι) => G.Adj (f i) (f j)

def SimpleGraph.IsCriticalEdges {V : Type u_1} (G : SimpleGraph V) (edges : Set (Sym2 V)) : Prop

A set of edges is critical if deleting them reduces the chromatic number.

Equations

• G.IsCriticalEdges edges = ((G.deleteEdges edges).chromaticNumber < G.chromaticNumber)

def SimpleGraph.IsCriticalEdge {V : Type u_1} (G : SimpleGraph V) (e : Sym2 V) : Prop

An edge is critical if deleting it reduces the chromatic number.

Equations

• G.IsCriticalEdge e = G.IsCriticalEdges {e}

def SimpleGraph.Subgraph.IsCriticalVerts {V : Type u_1} {G : SimpleGraph V} (verts : Set V) (G' : G.Subgraph) : Prop

A set of vertices is critical if deleting them reduces the chromatic number.

Equations

• SimpleGraph.Subgraph.IsCriticalVerts verts G' = ((G'.deleteVerts verts).coe.chromaticNumber < G'.coe.chromaticNumber)

def SimpleGraph.Subgraph.IsCriticalVertex {V : Type u_1} {G : SimpleGraph V} (v : V) (G' : G.Subgraph) : Prop

A vertex is critical if deleting it reduces the chromatic number.

Equations

• SimpleGraph.Subgraph.IsCriticalVertex v G' = SimpleGraph.Subgraph.IsCriticalVerts {v} G'

def SimpleGraph.IsCritical {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Prop

A graph G is k-critical (or vertex-critical) if its chromatic number is k, and deleting any single vertex reduces the chromatic number.

Equations

• G.IsCritical k = (G.chromaticNumber = ↑k ∧ ∀ (v : V), SimpleGraph.Subgraph.IsCriticalVertex v ⊤)

theorem SimpleGraph.not_isCritical_of_fintype_lt {V : Type u_1} (G : SimpleGraph V) [Fintype V] (k : ℕ) (hk : Fintype.card V < k) : ¬G.IsCritical k

theorem SimpleGraph.colorable_iff_induce_eq_bot {V : Type u_1} (G : SimpleGraph V) (n : ℕ) : G.Colorable n ↔ ∃ (coloring : V → Fin n), ∀ (i : Fin n), induce {v : V | coloring v = i} G = ⊥

def SimpleGraph.Cocolorable {V : Type u_1} (G : SimpleGraph V) (n : ℕ) : Prop

Equations

• G.Cocolorable n = ∃ (coloring : V → Fin n), ∀ (i : Fin n), SimpleGraph.induce {v : V | coloring v = i} G = ⊥ ∨ SimpleGraph.induce {v : V | coloring v = i} G = ⊤

noncomputable def SimpleGraph.cochromaticNumber {V : Type u_1} (G : SimpleGraph V) : ℕ∞

The chromatic number of a graph is the minimal number of colors needed to color it. This is ⊤ (infinity) iff G isn't colorable with finitely many colors.

If G is colorable, then ENat.toNat G.chromaticNumber is the ℕ-valued chromatic number.

Equations

• G.cochromaticNumber = ⨅ n ∈ setOf G.Cocolorable, ↑n

noncomputable def SimpleGraph.chromaticCardinal {V : Type u} (G : SimpleGraph V) : Cardinal.{u}

The chromatic cardinal is the minimal number of colors need to color it. In contrast to chromaticNumber, which assigns ⊤ : ℕ∞ to all non-finitely colorable graphs, this definition returns a Cardinal and can therefore distinguish between different infinite chromatic numbers.

Equations

• G.chromaticCardinal = sInf {κ : Cardinal.{?u.13} | ∃ (C : Type ?u.13) (_ : Cardinal.mk C = κ), Nonempty (G.Coloring C)}