Theorems · Definition · combinatorics

SimpleGraph.Coloring.mk

{V : Type u} →
  {G : SimpleGraph V} → {α : Type u_2} → (color : V → α) → (∀ {v w : V}, G.Adj v w → color v ≠ color w) → G.Coloring α

Construct a term of SimpleGraph.Coloring using a function that assigns vertices to colors and a proof that it is as proper coloring. (Note: this is a definitionally the constructor for SimpleGraph.Hom, but with a syntactically better proper coloring hypothesis.)

Defined in

Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Cited by

3 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound