Commit 2023-02-28 07:22 03cb3af0

View on Github →

feat Port/Combinatorics.SimpleGraph.Coloring (#2526)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Coloring.lean

added theorem SimpleGraph.Colorable.chromaticNumber_le_of_forall_imp

added theorem SimpleGraph.Colorable.chromaticNumber_mono

added theorem SimpleGraph.Colorable.chromaticNumber_mono_of_embedding

added theorem SimpleGraph.Colorable.mono

added theorem SimpleGraph.Colorable.mono_left

added theorem SimpleGraph.Colorable.of_embedding

added def SimpleGraph.Colorable

added theorem SimpleGraph.Coloring.card_colorClasses_le

added def SimpleGraph.Coloring.colorClass

added def SimpleGraph.Coloring.colorClasses

added theorem SimpleGraph.Coloring.colorClasses_finite

added theorem SimpleGraph.Coloring.colorClasses_isPartition

added theorem SimpleGraph.Coloring.color_classes_independent

added theorem SimpleGraph.Coloring.mem_colorClass

added theorem SimpleGraph.Coloring.mem_colorClasses

added def SimpleGraph.Coloring.mk

added theorem SimpleGraph.Coloring.not_adj_of_mem_colorClass

added theorem SimpleGraph.Coloring.to_colorable

added theorem SimpleGraph.Coloring.valid

added def SimpleGraph.CompleteBipartiteGraph.bicoloring

added theorem SimpleGraph.CompleteBipartiteGraph.chromaticNumber

added theorem SimpleGraph.IsClique.card_le_chromaticNumber

added theorem SimpleGraph.IsClique.card_le_of_colorable

added theorem SimpleGraph.IsClique.card_le_of_coloring

added theorem SimpleGraph.chromaticNumber_bddBelow

added theorem SimpleGraph.chromaticNumber_bot

added theorem SimpleGraph.chromaticNumber_eq_card_of_forall_surj

added theorem SimpleGraph.chromaticNumber_eq_zero_of_isempty

added theorem SimpleGraph.chromaticNumber_le_card

added theorem SimpleGraph.chromaticNumber_le_of_colorable

added theorem SimpleGraph.chromaticNumber_le_one_of_subsingleton

added theorem SimpleGraph.chromaticNumber_pos

added theorem SimpleGraph.chromaticNumber_top

added theorem SimpleGraph.chromaticNumber_top_eq_zero_of_infinite

added theorem SimpleGraph.cliqueFree_of_chromaticNumber_lt

added theorem SimpleGraph.colorable_chromaticNumber

added theorem SimpleGraph.colorable_chromaticNumber_of_fintype

added theorem SimpleGraph.colorable_iff_exists_bdd_nat_coloring

added theorem SimpleGraph.colorable_of_chromaticNumber_pos

added theorem SimpleGraph.colorable_of_fintype

added theorem SimpleGraph.colorable_of_isEmpty

added theorem SimpleGraph.colorable_set_nonempty_of_colorable

added def SimpleGraph.coloringOfIsEmpty

added theorem SimpleGraph.isEmpty_of_chromaticNumber_eq_zero

added theorem SimpleGraph.isEmpty_of_colorable_zero

added def SimpleGraph.recolorOfEmbedding

added def SimpleGraph.recolorOfEquiv

added def SimpleGraph.selfColoring