Commit 2023-02-28 12:11 ea5eff7d

View on Github →

feat: port Combinatorics.SimpleGraph.Partition (#2536)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Partition.lean

added def SimpleGraph.Coloring.toPartition

added def SimpleGraph.Partition.PartsCardLe

added theorem SimpleGraph.Partition.mem_partOfVertex

added def SimpleGraph.Partition.partOfVertex

added theorem SimpleGraph.Partition.partOfVertex_mem

added theorem SimpleGraph.Partition.partOfVertex_ne_of_adj

added def SimpleGraph.Partition.toColoring'

added def SimpleGraph.Partition.toColoring

added theorem SimpleGraph.Partition.to_colorable

added structure SimpleGraph.Partition

added def SimpleGraph.Partitionable

added theorem SimpleGraph.partitionable_iff_colorable