Commit 2024-03-22 14:25 1111ecb4

View on Github →

feat(SimpleGraph/Coloring): Surjectivity of graph colorings (#11397) Add two simple results on graph colorings with χ(G) colors.

If r ≤ χ(G) and C is an r-coloring of G then C is surjective
If G has an α-coloring then χ(G) = |α| iff every such coloring is surjective.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

added theorem SimpleGraph.card_le_chromaticNumber_iff_forall_surjective

added theorem SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective

deleted theorem SimpleGraph.chromaticNumber_eq_card_of_forall_surj

added theorem SimpleGraph.chromaticNumber_eq_iff_forall_surjective

added theorem SimpleGraph.coe_recolorOfCardLE

added theorem SimpleGraph.coe_recolorOfEmbedding

added theorem SimpleGraph.coe_recolorOfEquiv

added theorem SimpleGraph.le_chromaticNumber_iff_forall_surjective

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem SimpleGraph.Embedding.coe_completeGraph

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castLE_inj

added theorem Fin.castLE_injective