Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-04 03:25 2da25ede

View on Github →

feat(combinatorics/simple_graph): Graph coloring and partitions (#10287)

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added def complete_bipartite_graph

added def simple_graph.embedding.complete_graph.of_embedding

added def simple_graph.hom.map_spanning_subgraphs

Created src/combinatorics/simple_graph/coloring.lean

added theorem simple_graph.chromatic_number_bdd_below

added theorem simple_graph.chromatic_number_bot

added theorem simple_graph.chromatic_number_complete_graph

added theorem simple_graph.chromatic_number_eq_card_of_forall_surj

added theorem simple_graph.chromatic_number_eq_zero_of_isempty

added theorem simple_graph.chromatic_number_le_card

added theorem simple_graph.chromatic_number_le_of_colorable

added theorem simple_graph.chromatic_number_le_of_forall_imp

added theorem simple_graph.chromatic_number_le_of_le_colorable

added theorem simple_graph.chromatic_number_le_one_of_subsingleton

added theorem simple_graph.colorable.of_le

added def simple_graph.colorable

added theorem simple_graph.colorable_chromatic_number

added theorem simple_graph.colorable_chromatic_number_of_fintype

added theorem simple_graph.colorable_iff_exists_bdd_nat_coloring

added theorem simple_graph.colorable_of_fintype

added theorem simple_graph.colorable_of_is_empty

added theorem simple_graph.colorable_of_le_colorable

added theorem simple_graph.colorable_set_nonempty_of_colorable

added theorem simple_graph.coloring.card_color_classes_le

added def simple_graph.coloring.color_class

added def simple_graph.coloring.color_classes

added theorem simple_graph.coloring.color_classes_finite_of_fintype

added theorem simple_graph.coloring.color_classes_independent

added theorem simple_graph.coloring.color_classes_is_partition

added theorem simple_graph.coloring.mem_color_class

added theorem simple_graph.coloring.mem_color_classes

added def simple_graph.coloring.mk

added theorem simple_graph.coloring.not_adj_of_mem_color_class

added theorem simple_graph.coloring.to_colorable

added theorem simple_graph.coloring.valid

added def simple_graph.coloring

added def simple_graph.coloring_of_is_empty

added def simple_graph.complete_bipartite_graph.bicoloring

added theorem simple_graph.complete_bipartite_graph.chromatic_number

added theorem simple_graph.is_empty_of_chromatic_number_eq_zero

added theorem simple_graph.is_empty_of_colorable_zero

added def simple_graph.recolor_of_embedding

added def simple_graph.recolor_of_equiv

added def simple_graph.self_coloring

added theorem simple_graph.zero_lt_chromatic_number

Created src/combinatorics/simple_graph/partition.lean

added def simple_graph.coloring.to_partition

added theorem simple_graph.partition.mem_part_of_vertex

added def simple_graph.partition.part_of_vertex

added theorem simple_graph.partition.part_of_vertex_mem

added theorem simple_graph.partition.part_of_vertex_ne_of_adj

added def simple_graph.partition.parts_card_le

added theorem simple_graph.partition.to_colorable

added def simple_graph.partition.to_coloring'

added def simple_graph.partition.to_coloring

added structure simple_graph.partition

added def simple_graph.partitionable

added theorem simple_graph.partitionable_iff_colorable

Modified src/data/fintype/basic.lean

added theorem fintype.card_range_le

Modified src/data/setoid/partition.lean

added theorem setoid.card_classes_ker_le

added theorem setoid.classes_ker_subset_fiber_set

added theorem setoid.nonempty_fintype_classes_ker