Lax9.ChiBoundedness

χ-Boundedness

concepts/Lax9/ChiBoundedness.lean · Lax9

nothing to prove

A class of finite simple graphs is χ-bounded if the chromatic number of each graph in the class is bounded by a function of its clique number.

1	import Lax9.MergeWidth
2
3	/-!
4	---
5	title: χ-Boundedness
6	type: definition
7	---
8	A class of finite simple graphs is χ-bounded if the chromatic number of each
9	graph in the class is bounded by a function of its clique number.
10	-/
11
12	namespace Lax9.ChiBoundedness
13
14	open Lax9.MergeWidth
15
16	/-- A graph class $C$ is χ-bounded if there is a function $f$ such that every
17	$G ∈ C$ is $f(ω(G))$-colourable. -/
18	def ChiBounded (C : GraphClass) : Prop :=
19	∃ f : ℕ → ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G →
20	G.Colorable (f G.cliqueNum)
21
22	end Lax9.ChiBoundedness
23

none