Theorems · Theorem · combinatorics

SimpleGraph.coe_recolorOfCardLE

∀ {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β]
  (hαβ : Fintype.card α ≤ Fintype.card β),
  ⇑(G.recolorOfCardLE hαβ) = (SimpleGraph.Embedding.completeGraph ⋯.some).toHom.comp

Defined in

Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintype