Partition

📁 Source: Mathlib/Combinatorics/SimpleGraph/Partition.lean

Statistics

Metric	Count
Definitions toPartition, Partition, PartsCardLe, instInhabited, partOfVertex, parts, toColoring, toColoring', Partitionable	9
Theorems toPartition_parts, colorable, default_def, independent, isPartition, mem_partOfVertex, partOfVertex_mem, partOfVertex_ne_of_adj, partitionable_iff_colorable	9
Total	18

SimpleGraph

Definitions

Name	Category	Theorems
Partition 📖	CompData	1 math math: Partition.default_def
Partitionable 📖	MathDef	1 math math: partitionable_iff_colorable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partitionable_iff_colorable 📖	mathematical	—	Partitionable Colorable	—	Colorable.mono Set.Finite.card_toFinset Partition.colorable Coloring.colorClasses_finite Finite.of_fintype le_trans Coloring.card_colorClasses_le Eq.le Fintype.card_fin

SimpleGraph.Coloring

Definitions

Name	Category	Theorems
toPartition 📖	CompOp	2 math math: SimpleGraph.Partition.default_def, toPartition_parts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPartition_parts 📖	mathematical	—	SimpleGraph.Partition.parts toPartition colorClasses	—	—

SimpleGraph.Partition

Definitions

Name	Category	Theorems
PartsCardLe 📖	MathDef	—
instInhabited 📖	CompOp	1 math math: default_def
partOfVertex 📖	CompOp	2 math math: partOfVertex_mem, mem_partOfVertex
parts 📖	CompOp	4 math math: isPartition, colorable, partOfVertex_mem, SimpleGraph.Coloring.toPartition_parts
toColoring 📖	CompOp	—
toColoring' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colorable 📖	mathematical	—	SimpleGraph.Colorable Fintype.card Set.Elem Set parts	—	SimpleGraph.Coloring.colorable
default_def 📖	mathematical	—	SimpleGraph.Partition instInhabited SimpleGraph.Coloring.toPartition SimpleGraph.selfColoring	—	—
independent 📖	mathematical	Set Set.instMembership parts	IsAntichain SimpleGraph.Adj	—	—
isPartition 📖	mathematical	—	Setoid.IsPartition parts	—	—
mem_partOfVertex 📖	mathematical	—	Set Set.instMembership partOfVertex	—	isPartition
partOfVertex_mem 📖	mathematical	—	Set Set.instMembership parts partOfVertex	—	isPartition
partOfVertex_ne_of_adj 📖	—	SimpleGraph.Adj	—	—	mem_partOfVertex independent partOfVertex_mem SimpleGraph.ne_of_adj

---

← Back to Index