def SimpleGraph.«termχ(_)» : Lean.ParserDescr

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

• One or more equations did not get rendered due to their size.

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.lt_chromaticNumber_iff_not_colorable {V : Type u_1} {G : SimpleGraph V} {n : ℕ} : ↑n < G.chromaticNumber ↔ ¬G.Colorable n

theorem SimpleGraph.le_chromaticNumber_iff_not_colorable {V : Type u_1} {G : SimpleGraph V} {n : ℕ} (hn : n ≠ 0) : ↑n ≤ G.chromaticNumber ↔ ¬G.Colorable (n - 1)

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

theorem SimpleGraph.card_div_indepNum_le_chromaticNumber {V : Type u_1} {G : SimpleGraph V} : ↑⌈↑(Nat.card V) / ↑G.indepNum⌉₊ ≤ G.chromaticNumber

instance SimpleGraph.instSymmAdj_formalConjecturesForMathlib {V : Type u_1} {ι : Type u_3} {G : SimpleGraph V} (f : ι → V) : Std.Symm 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)}

noncomputable def SimpleGraph.indepNumK {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : ℕ

The maximum size of the union of k finite independent sets.

Equations

• G.indepNumK k = sSup {n : ℕ | ∃ (f : Fin k → Set V), (∀ (i : Fin k), G.IsIndepSet (f i)) ∧ (⋃ (i : Fin k), f i).ncard = n}

def SimpleGraph.CDSColorable {α : Type u_2} [Fintype α] {G : SimpleGraph α} : Prop

A finite graph is CDS-colorable if it has a proper coloring by natural numbers such that for all k > 0, the number of vertices with color < k equals the maximum size of the union of k independent sets.

Equations

• SimpleGraph.CDSColorable = ∃ (C : G.Coloring ℕ), ∀ (k : ℕ), ∑ i ∈ Finset.Iio k, (C.colorClass i).ncard = G.indepNumK k

def SimpleGraph.IsRainbow {α : Type u_4} {V : Type u_5} {H : SimpleGraph α} {G : SimpleGraph V} (f : H →g G) {C : Type u_6} (c : Sym2 V → C) : Prop

A homomorphism is rainbow if it maps distinct edges to distinct colors.

Equations

• SimpleGraph.IsRainbow f c = Function.Injective fun (e : ↑H.edgeSet) => c (Sym2.map ⇑f ↑e)

noncomputable def SimpleGraph.antiRamseyNum {α : Type u_4} [Fintype α] (H : SimpleGraph α) (n : ℕ) : ℕ

The anti-Ramsey number $\mathrm{AR}(n, H)$: maximum colors to edge-color $K_n$ without rainbow $H$.

Equations

• H.antiRamseyNum n = sSup {k : ℕ | ∃ (c : Sym2 (Fin n) → Fin k), ∀ (f : H →g ⊤), ¬SimpleGraph.IsRainbow f c}