SimpleGraph.colorable_chromaticNumber
theorem SimpleGraph.colorable_chromaticNumber :
∀ {V : Type u} {G : SimpleGraph V} {m : ℕ}, G.Colorable m → G.Colorable (ENat.toNat G.chromaticNumber)
The theorem `SimpleGraph.colorable_chromaticNumber` states that for any given type `V`, simple graph `G` of the same type, and natural number `m`, if the graph `G` is colorable with `m` colors, then it is also colorable with the number of colors equal to the natural number representation of its chromatic number. The chromatic number of a graph is the minimum number of colors needed to color the graph, and `ENat.toNat` is a function converting extended natural numbers to natural numbers, where infinity is mapped to zero.
More concisely: If a simple graph of type `V` is colorable with `m` colors and its chromatic number is `n`, then it is also colorable with `n` (or `ENat.toNat n` in Lean) colors.
|
SimpleGraph.Colorable.chromaticNumber_eq_sInf
theorem SimpleGraph.Colorable.chromaticNumber_eq_sInf :
∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n → G.chromaticNumber = ↑(sInf {n' | G.Colorable n'}) := by
sorry
The theorem `SimpleGraph.Colorable.chromaticNumber_eq_sInf` states that for any type `V`, any simple graph `G` of type `V`, and any natural number `n`, if the graph `G` can be colored with at most `n` colors i.e., `G` is `n`-colorable, then the chromatic number of the graph `G` is equal to the infimum of the set of all natural numbers `n'` such that `G` is `n'`-colorable. In other words, the chromatic number of a simple graph is the smallest number of colors needed to color the graph, in terms of the least element of the set of all natural numbers that color the graph.
More concisely: The chromatic number of a simple graph is the smallest natural number sufficient for its coloring.
|
SimpleGraph.colorable_set_nonempty_of_colorable
theorem SimpleGraph.colorable_set_nonempty_of_colorable :
∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n → {n | G.Colorable n}.Nonempty
This theorem states that for any given type `V`, any simple graph `G` of type `V`, and any natural number `n`, if the graph `G` can be colored using at most `n` colors (which is represented by `SimpleGraph.Colorable G n`), then there exists at least one `n` such that the graph `G` can be colored by `n` colors. In other words, the set of those `n` for which `G` can be colored by `n` colors is nonempty. This theorem provides a link between the colorability of a graph and the existence of a coloring number within a specific set.
More concisely: If a simple graph `G` of type `V` is `n`-colorable, then there exists a valid `n`-coloring for `G`.
|
SimpleGraph.Coloring.colorable
theorem SimpleGraph.Coloring.colorable :
∀ {V : Type u} {G : SimpleGraph V} {α : Type u_1} [inst : Fintype α], G.Coloring α → G.Colorable (Fintype.card α)
The theorem `SimpleGraph.Coloring.colorable` states that for any given type `V`, a simple graph `G` of type `V`, and another type `α`, if `α` is a finite type, then if there exists a coloring of graph `G` with elements of `α`, it implies that the graph `G` is colorable with at most as many colors as there are elements in `α`. In terms of graph theory, it says that if you can properly color a graph using certain colors from a finite set, then the graph is considered colorable with a maximum color count equal to the size of that set.
More concisely: If a simple graph of finite type `V` admits a coloring using at most `α.size` colors, then it is colorable.
|
SimpleGraph.chromaticNumber_le_iff_colorable
theorem SimpleGraph.chromaticNumber_le_iff_colorable :
∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.chromaticNumber ≤ ↑n ↔ G.Colorable n
The theorem `SimpleGraph.chromaticNumber_le_iff_colorable` states that for any graph `G` of type `SimpleGraph V` and for any natural number `n`, the chromatic number of `G` is less than or equal to `n` if and only if `G` can be colored with at most `n` colors. Here, the chromatic number of a graph is the minimum number of colors needed to color that graph, and a graph is considered colorable with at most `n` colors if there exists a coloring of the graph using `n` or fewer colors.
More concisely: The chromatic number of a simple graph `G` equals or is less than a natural number `n` if and only if `G` is colorable using at most `n` colors.
|
SimpleGraph.chromaticNumber_ne_top_iff_exists
theorem SimpleGraph.chromaticNumber_ne_top_iff_exists :
∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n
This theorem states that for any given type `V` and a simple graph `G` of type `V`, the chromatic number of `G` is not infinite if and only if there exists some natural number `n` such that the graph `G` can be colored with at most `n` colors. In other words, a graph has a finite chromatic number if it can be colored with a finite number of colors, and vice versa.
More concisely: The chromatic number of a simple graph is finite if and only if the graph can be colored using a finite number of colors.
|
SimpleGraph.Coloring.valid
theorem SimpleGraph.Coloring.valid :
∀ {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {v w : V}, G.Adj v w → C v ≠ C w
The theorem `SimpleGraph.Coloring.valid` states that for any type `V`, any simple graph `G` of type `V`, any type `α`, and any `α`-coloring `C` of the graph `G`, if `v` and `w` are vertices in `G` such that `v` is adjacent to `w` (expressed as `G.Adj v w`), then the colors of `v` and `w` under the coloring `C` are different. This theorem captures a key property of graph coloring: no two adjacent vertices share the same color.
More concisely: In any simple graph and any valid coloring, adjacent vertices have distinct colors.
|