Theorems · Definition · combinatorics

SimpleGraph.recolorOfCardLE

{V : Type u} →
  (G : SimpleGraph V) →
    {α : Type u_4} →
      {β : Type u_5} →
        [inst : Fintype α] → [inst_1 : Fintype β] → Fintype.card α ≤ Fintype.card β → G.Coloring α ↪ G.Coloring β

There is a noncomputable embedding of α-colorings to β-colorings if β has at least as large a cardinality as α.

Defined in

Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Cited by

4 results in Mathlib

Foundations

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

Assumes

FintypeFintype