Mathlib Changelog
v3
Changelog
About
Github
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