Coloring

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

Statistics

Metric	Count
Definitions `Colorable`, `toColoring`, `Coloring`, `colorClass`, `colorClasses`, `mk`, `ofIsEmpty`, `bicoloring`, `chromaticNumber`, `coloringOfIsEmpty`, `coloring`, `instDecidablePredMemSetColorClassOfDecidableEq`, `instFintypeColoring`, `recolorOfCardLE`, `recolorOfEmbedding`, `recolorOfEquiv`, `selfColoring`	17
Theorems `card_le_of_pairwise_adj`, `chromaticNumber_eq_sInf`, `chromaticNumber_le`, `cliqueFree`, `map`, `mono`, `mono_left`, `of_embedding`, `of_hom`, `of_isEmpty`, `card_colorClasses_le`, `colorClasses_finite`, `colorClasses_isPartition`, `color_classes_independent`, `colorable`, `injective_comp_of_pairwise_adj`, `mem_colorClass`, `mem_colorClasses`, `not_adj_of_mem_colorClass`, `surjOn_of_card_le_isClique`, `valid`, `chromaticNumber`, `card_le_chromaticNumber`, `card_le_of_colorable`, `card_le_of_coloring`, `card_le_chromaticNumber_iff_forall_surjective`, `chromaticNumber_bddBelow`, `chromaticNumber_bot`, `chromaticNumber_eq_biInf`, `chromaticNumber_eq_card_iff`, `chromaticNumber_eq_card_iff_forall_surjective`, `chromaticNumber_eq_iInf`, `chromaticNumber_eq_iff_colorable_not_colorable`, `chromaticNumber_eq_iff_forall_surjective`, `chromaticNumber_eq_one_iff`, `chromaticNumber_eq_zero_of_isEmpty`, `chromaticNumber_eq_zero_of_isempty`, `chromaticNumber_le_card`, `chromaticNumber_le_iff_colorable`, `chromaticNumber_le_of_forall_imp`, `chromaticNumber_le_one_of_subsingleton`, `chromaticNumber_mono`, `chromaticNumber_mono_of_embedding`, `chromaticNumber_mono_of_hom`, `chromaticNumber_ne_top_iff_exists`, `chromaticNumber_pos`, `chromaticNumber_top`, `chromaticNumber_top_eq_top_of_infinite`, `cliqueFree_of_chromaticNumber_lt`, `cliqueNum_le_chromaticNumber`, `coe_recolorOfCardLE`, `coe_recolorOfEmbedding`, `coe_recolorOfEquiv`, `colorableOfIsEmpty`, `colorable_chromaticNumber`, `colorable_chromaticNumber_of_fintype`, `colorable_iff_exists_bdd_nat_coloring`, `colorable_iff_forall_connectedComponents`, `colorable_of_chromaticNumber_ne_top`, `colorable_of_fintype`, `colorable_set_nonempty_of_colorable`, `colorable_zero_iff`, `chromaticNumber`, `colorable`, `colorable_of_cliqueFree`, `eq_top_of_chromaticNumber_eq_card`, `free_of_colorable`, `instInfiniteColoringOfNonempty`, `instNontrivialColoringOfNonempty`, `isEmpty_of_chromaticNumber_eq_zero`, `isEmpty_of_colorable_zero`, `le_chromaticNumber_iff_colorable`, `le_chromaticNumber_iff_coloring`, `le_chromaticNumber_iff_forall_surjective`, `le_chromaticNumber_of_pairwise_adj`, `two_le_chromaticNumber_iff_ne_bot`, `two_le_chromaticNumber_of_adj`	77
Total	94

SimpleGraph

Definitions

Name	Category	Theorems
`Colorable` 📖	MathDef	37 math math: `colorable_iff_forall_connectedComponents`, `partitionable_iff_colorable`, `completeEquipartiteGraph_colorable`, `IsFiveWheelLike.not_colorable_succ`, `Colorable.of_isEmpty`, `Colorable.of_hom`, `colorable_chromaticNumber`, `Colorable.of_sum_right`, `Colorable.mono`, `Colorable.chromaticNumber_eq_sInf`, `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree`, `Partition.colorable`, `Colorable.of_sum_left`, `chromaticNumber_eq_iInf`, `colorable_sum`, `Colorable.sum_max`, `chromaticNumber_le_iff_colorable`, `chromaticNumber_eq_iff_colorable_not_colorable`, `colorable_iff_exists_bdd_nat_coloring`, `colorable_of_cliqueFree_lt_minDegree`, `chromaticNumber_ne_top_iff_exists`, `Colorable.mono_left`, `Colorable.of_embedding`, `chromaticNumber_eq_biInf`, `two_colorable_iff_forall_loop_even`, `Colorable.map`, `IsCompleteMultipartite.colorable_of_cliqueFree`, `completeMultipartiteGraph.colorable`, `colorable_chromaticNumber_of_fintype`, `chromaticNumber_bddBelow`, `colorable_zero_iff`, `colorable_set_nonempty_of_colorable`, `completeMultipartiteGraph.colorable_of_cliqueFree`, `Coloring.colorable`, `colorableOfIsEmpty`, `colorable_of_chromaticNumber_ne_top`, `colorable_of_fintype`
`Coloring` 📖	CompOp	16 math math: `Coloring.mem_colorClass`, `card_le_chromaticNumber_iff_forall_surjective`, `le_chromaticNumber_iff_forall_surjective`, `Coloring.injective_comp_of_pairwise_adj`, `instInfiniteColoringOfNonempty`, `colorable_iff_exists_bdd_nat_coloring`, `coe_recolorOfEmbedding`, `coe_recolorOfEquiv`, `instNontrivialColoringOfNonempty`, `Coloring.surjOn_of_card_le_isClique`, `Coloring.odd_length_iff_not_congr`, `chromaticNumber_eq_iff_forall_surjective`, `Coloring.mem_colorClasses`, `coe_recolorOfCardLE`, `Coloring.even_length_iff_congr`, `chromaticNumber_eq_card_iff_forall_surjective`
`chromaticNumber` 📖	CompOp	45 math math: `le_chromaticNumber_iff_colorable`, `le_chromaticNumber_iff_coloring`, `chromaticNumber_pos`, `two_le_chromaticNumber_of_adj`, `card_le_chromaticNumber_iff_forall_surjective`, `colorable_chromaticNumber`, `chromaticNumber_cycleGraph_of_even`, `chromaticNumber_le_sum_right`, `chromaticNumber_mono_of_embedding`, `chromaticNumber_top`, `Colorable.chromaticNumber_eq_sInf`, `chromaticNumber_le_of_forall_imp`, `chromaticNumber_eq_zero_of_isEmpty`, `chromaticNumber_eq_iInf`, `chromaticNumber_sum`, `chromaticNumber_le_card`, `chromaticNumber_eq_two_iff`, `chromaticNumber_le_iff_colorable`, `chromaticNumber_eq_iff_colorable_not_colorable`, `chromaticNumber_eq_card_iff`, `chromaticNumber_le_two_iff_isBipartite`, `CompleteBipartiteGraph.chromaticNumber`, `two_le_chromaticNumber_iff_ne_bot`, `le_chromaticNumber_iff_forall_surjective`, `Colorable.chromaticNumber_le`, `cliqueNum_le_chromaticNumber`, `chromaticNumber_cycleGraph_of_odd`, `chromaticNumber_le_one_of_subsingleton`, `le_chromaticNumber_of_pairwise_adj`, `chromaticNumber_mono`, `chromaticNumber_eq_zero_of_isempty`, `completeMultipartiteGraph.chromaticNumber`, `chromaticNumber_eq_biInf`, `chromaticNumber_top_eq_top_of_infinite`, `chromaticNumber_le_sum_left`, `IsClique.card_le_chromaticNumber`, `chromaticNumber_eq_iff_forall_surjective`, `colorable_chromaticNumber_of_fintype`, `chromaticNumber_pathGraph`, `Walk.three_le_chromaticNumber_of_odd_loop`, `chromaticNumber_mono_of_hom`, `chromaticNumber_eq_one_iff`, `chromaticNumber_eq_card_iff_forall_surjective`, `colorable_of_chromaticNumber_ne_top`, `chromaticNumber_bot`
`coloringOfIsEmpty` 📖	CompOp	—
`instDecidablePredMemSetColorClassOfDecidableEq` 📖	CompOp	—
`instFintypeColoring` 📖	CompOp	—
`recolorOfCardLE` 📖	CompOp	1 math math: `coe_recolorOfCardLE`
`recolorOfEmbedding` 📖	CompOp	1 math math: `coe_recolorOfEmbedding`
`recolorOfEquiv` 📖	CompOp	1 math math: `coe_recolorOfEquiv`
`selfColoring` 📖	CompOp	1 math math: `Partition.default_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_chromaticNumber_iff_forall_surjective` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `Fintype.card` `chromaticNumber` `DFunLike.coe` `Coloring` `RelHom.instFunLike` `Adj` `completeGraph`	—	`Coloring.valid` `Nat.notMem_of_lt_sInf` `LT.lt.trans_le` `Fintype.card_pos_iff` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Colorable.chromaticNumber_eq_sInf` `Coloring.colorable` `Fintype.card_subtype_compl` `Fintype.card_unique` `Fintype.card_fin` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `LT.lt.le` `LT.lt.not_ge` `Fintype.card_le_of_surjective` `Function.Embedding.nonempty_of_card_le` `Function.Surjective.of_comp`
`chromaticNumber_bddBelow` 📖	mathematical	—	`BddBelow` `setOf` `Colorable`	—	`zero_le` `Nat.instCanonicallyOrderedAdd`
`chromaticNumber_bot` 📖	mathematical	—	`chromaticNumber` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`LE.le.antisymm` `Colorable.chromaticNumber_le` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `chromaticNumber_pos`
`chromaticNumber_eq_biInf` 📖	mathematical	—	`chromaticNumber` `iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership` `setOf` `Colorable` `ENat.instNatCast`	—	—
`chromaticNumber_eq_card_iff` 📖	mathematical	—	`chromaticNumber` `ENat` `ENat.instNatCast` `Fintype.card` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`eq_top_of_chromaticNumber_eq_card` `chromaticNumber_top`
`chromaticNumber_eq_card_iff_forall_surjective` 📖	mathematical	—	`chromaticNumber` `ENat` `ENat.instNatCast` `Fintype.card` `DFunLike.coe` `Coloring` `RelHom.instFunLike` `Adj` `completeGraph`	—	`LE.le.ge_iff_eq` `Colorable.chromaticNumber_le` `card_le_chromaticNumber_iff_forall_surjective`
`chromaticNumber_eq_iInf` 📖	mathematical	—	`chromaticNumber` `iInf` `ENat` `Set.Elem` `setOf` `Colorable` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ENat.instNatCast` `Set` `Set.instMembership`	—	`chromaticNumber.eq_1` `iInf_subtype`
`chromaticNumber_eq_iff_colorable_not_colorable` 📖	mathematical	—	`chromaticNumber` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Colorable`	—	`eq_iff_le_not_lt` `not_lt` `ENat.add_one_le_iff` `ENat.coe_ne_top` `not_le` `chromaticNumber_le_iff_colorable` `Nat.cast_add_one`
`chromaticNumber_eq_iff_forall_surjective` 📖	mathematical	—	`chromaticNumber` `ENat` `ENat.instNatCast` `DFunLike.coe` `Coloring` `RelHom.instFunLike` `Adj` `completeGraph`	—	`LE.le.ge_iff_eq` `Colorable.chromaticNumber_le` `le_chromaticNumber_iff_forall_surjective`
`chromaticNumber_eq_one_iff` 📖	mathematical	—	`chromaticNumber` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `ne_bot_iff_exists_adj` `Nat.instAtLeastTwoHAddOfNat` `two_le_chromaticNumber_of_adj` `Mathlib.Tactic.Contrapose.contrapose₃` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `not_isEmpty_iff` `Colorable.chromaticNumber_le` `colorable_zero_iff` `Nat.cast_zero` `NeZero.one` `chromaticNumber_bot`
`chromaticNumber_eq_zero_of_isEmpty` 📖	mathematical	—	`chromaticNumber` `ENat` `instZeroENat`	—	`nonpos_iff_eq_zero` `Nat.cast_zero` `chromaticNumber_le_iff_colorable` `Colorable.of_isEmpty`
`chromaticNumber_eq_zero_of_isempty` 📖	mathematical	—	`chromaticNumber` `ENat` `instZeroENat`	—	`chromaticNumber_eq_zero_of_isEmpty`
`chromaticNumber_le_card` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `ENat.instNatCast` `Fintype.card`	—	`chromaticNumber_top` `chromaticNumber_mono_of_hom`
`chromaticNumber_le_iff_colorable` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `ENat.instNatCast` `Colorable`	—	`LT.lt.ne` `WithTop.coe_lt_top` `chromaticNumber_ne_top_iff_exists` `Nat.sInf_mem` `Colorable.mono` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Colorable.chromaticNumber_eq_sInf` `Set.mem_setOf_eq` `Colorable.chromaticNumber_le`
`chromaticNumber_le_of_forall_imp` 📖	mathematical	`Colorable`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber`	—	`chromaticNumber.eq_1` `chromaticNumber_le_iff_colorable`
`chromaticNumber_le_one_of_subsingleton` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one` `chromaticNumber_le_iff_colorable`
`chromaticNumber_mono` 📖	mathematical	`SimpleGraph` `instLE`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber`	—	`chromaticNumber_le_of_forall_imp` `Colorable.mono_left`
`chromaticNumber_mono_of_embedding` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber`	—	`chromaticNumber_mono_of_hom`
`chromaticNumber_mono_of_hom` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber`	—	`chromaticNumber_le_of_forall_imp` `Colorable.of_hom`
`chromaticNumber_ne_top_iff_exists` 📖	mathematical	—	`Colorable`	—	`chromaticNumber.eq_1` `iInf_subtype` `lt_top_iff_ne_top` `ENat.iInf_coe_lt_top`
`chromaticNumber_pos` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instZeroENat` `chromaticNumber`	—	`Colorable.chromaticNumber_eq_sInf` `Nat.cast_pos` `le_csInf` `colorable_set_nonempty_of_colorable` `lt_of_lt_of_le`
`chromaticNumber_top` 📖	mathematical	—	`chromaticNumber` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `ENat.instNatCast` `Fintype.card`	—	`chromaticNumber_eq_card_iff_forall_surjective` `Coloring.colorable` `Finite.injective_iff_surjective` `Finite.of_fintype` `Mathlib.Tactic.Contrapose.contrapose₁` `Coloring.valid`
`chromaticNumber_top_eq_top_of_infinite` 📖	mathematical	—	`chromaticNumber` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `instTopENat`	—	`chromaticNumber_ne_top_iff_exists` `not_injective_infinite_finite` `Finite.of_fintype` `Hom.injective_of_top_hom`
`cliqueFree_of_chromaticNumber_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `ENat.instNatCast`	`CliqueFree`	—	`LT.lt.ne_top` `chromaticNumber_ne_top_iff_exists` `colorable_chromaticNumber` `Colorable.cliqueFree` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENat.coe_toNat_eq_self`
`cliqueNum_le_chromaticNumber` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `cliqueNum` `chromaticNumber`	—	`exists_isNClique_cliqueNum` `IsClique.card_le_chromaticNumber` `IsNClique.isClique` `IsNClique.card_eq`
`coe_recolorOfCardLE` 📖	mathematical	`Fintype.card`	`DFunLike.coe` `Function.Embedding` `Coloring` `Function.instFunLikeEmbedding` `recolorOfCardLE` `Hom.comp` `completeGraph` `Embedding.toHom` `Embedding.completeGraph` `Nonempty.some` `Function.Embedding.nonempty_of_card_le`	—	—
`coe_recolorOfEmbedding` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Coloring` `Function.instFunLikeEmbedding` `recolorOfEmbedding` `Hom.comp` `completeGraph` `Embedding.toHom` `Embedding.completeGraph`	—	—
`coe_recolorOfEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Coloring` `EquivLike.toFunLike` `Equiv.instEquivLike` `recolorOfEquiv` `Hom.comp` `completeGraph` `Embedding.toHom` `Embedding.completeGraph` `Equiv.toEmbedding`	—	—
`colorableOfIsEmpty` 📖	mathematical	—	`Colorable`	—	`Colorable.of_isEmpty`
`colorable_chromaticNumber` 📖	mathematical	—	`Colorable` `ENat.toNat` `chromaticNumber`	—	`Colorable.chromaticNumber_eq_sInf` `colorable_set_nonempty_of_colorable` `Nat.sInf_def` `Nat.find_spec`
`colorable_chromaticNumber_of_fintype` 📖	mathematical	—	`Colorable` `ENat.toNat` `chromaticNumber`	—	`nonempty_fintype` `colorable_chromaticNumber` `colorable_of_fintype`
`colorable_iff_exists_bdd_nat_coloring` 📖	mathematical	—	`Colorable` `DFunLike.coe` `Coloring` `RelHom.instFunLike` `Adj` `completeGraph`	—	`Fintype.card_fin` `Coloring.valid`
`colorable_iff_forall_connectedComponents` 📖	mathematical	—	`Colorable` `ConnectedComponent` `SetLike.instMembership` `ConnectedComponent.instSetLike` `ConnectedComponent.toSimpleGraph`	—	`Coloring.valid`
`colorable_of_chromaticNumber_ne_top` 📖	mathematical	—	`Colorable` `ENat.toNat` `chromaticNumber`	—	`chromaticNumber_ne_top_iff_exists` `colorable_chromaticNumber`
`colorable_of_fintype` 📖	mathematical	—	`Colorable` `Fintype.card`	—	`Coloring.colorable`
`colorable_set_nonempty_of_colorable` 📖	mathematical	—	`Set.Nonempty` `setOf` `Colorable`	—	—
`colorable_zero_iff` 📖	mathematical	—	`Colorable` `IsEmpty`	—	`isEmpty_of_colorable_zero` `Colorable.of_isEmpty`
`eq_top_of_chromaticNumber_eq_card` 📖	mathematical	`chromaticNumber` `ENat` `ENat.instNatCast` `Fintype.card`	`Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`ne_top_iff_exists_not_adj` `chromaticNumber_le_iff_colorable` `Fintype.card_congr'` `Fintype.card_subtype_compl` `Fintype.card_unique` `Coloring.colorable` `Fintype.one_lt_card_iff_nontrivial` `nontrivial_iff` `ENat.coe_le_coe` `ENat.coe_sub` `ENat.coe_one`
`free_of_colorable` 📖	mathematical	`Colorable`	`Free`	—	`Mathlib.Tactic.Contrapose.contrapose₄`
`instInfiniteColoringOfNonempty` 📖	mathematical	—	`Infinite` `Coloring`	—	`Infinite.of_injective`
`instNontrivialColoringOfNonempty` 📖	mathematical	—	`Nontrivial` `Coloring`	—	`nontrivial_iff_exists_ne`
`isEmpty_of_chromaticNumber_eq_zero` 📖	mathematical	`chromaticNumber` `ENat` `instZeroENat`	`IsEmpty`	—	`colorable_of_chromaticNumber_ne_top` `ENat.zero_ne_top` `isEmpty_of_colorable_zero`
`isEmpty_of_colorable_zero` 📖	mathematical	—	`IsEmpty`	—	—
`le_chromaticNumber_iff_colorable` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `chromaticNumber`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`le_chromaticNumber_iff_coloring` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `chromaticNumber`	—	—
`le_chromaticNumber_iff_forall_surjective` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `chromaticNumber` `DFunLike.coe` `Coloring` `RelHom.instFunLike` `Adj` `completeGraph`	—	`Fintype.card_fin`
`le_chromaticNumber_of_pairwise_adj` 📖	mathematical	`Nat.card` `Pairwise` `Adj`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `chromaticNumber`	—	`le_chromaticNumber_iff_colorable` `LE.le.trans` `Colorable.card_le_of_pairwise_adj`
`two_le_chromaticNumber_iff_ne_bot` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `chromaticNumber`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Contrapose.contrapose₃` `chromaticNumber_eq_zero_of_isEmpty` `chromaticNumber_eq_one_iff` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ne_bot_iff_exists_adj` `two_le_chromaticNumber_of_adj`
`two_le_chromaticNumber_of_adj` 📖	mathematical	`Adj`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `chromaticNumber`	—	`le_of_not_gt` `Nat.instAtLeastTwoHAddOfNat` `chromaticNumber_le_iff_colorable` `Order.le_of_lt_add_one` `Coloring.valid`

SimpleGraph.Colorable

Definitions

Name	Category	Theorems
`toColoring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_of_pairwise_adj` 📖	mathematical	`Pairwise` `SimpleGraph.Adj`	`Nat.card`	—	`Nat.card_eq_fintype_card` `Fintype.card_fin` `Nat.card_le_card_of_injective` `Finite.of_fintype` `SimpleGraph.Coloring.injective_comp_of_pairwise_adj`
`chromaticNumber_eq_sInf` 📖	mathematical	—	`SimpleGraph.chromaticNumber` `ENat` `ENat.instNatCast` `InfSet.sInf` `Nat.instInfSet` `setOf` `SimpleGraph.Colorable`	—	`ENat.coe_sInf` `SimpleGraph.chromaticNumber.eq_1`
`chromaticNumber_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SimpleGraph.chromaticNumber` `ENat.instNatCast`	—	`chromaticNumber_eq_sInf` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `csInf_le` `SimpleGraph.chromaticNumber_bddBelow`
`cliqueFree` 📖	mathematical	—	`SimpleGraph.CliqueFree`	—	`SimpleGraph.IsClique.card_le_of_colorable`
`map` 📖	mathematical	—	`SimpleGraph.Colorable` `SimpleGraph.map`	—	`Function.Injective.extend_apply` `Function.Embedding.injective` `SimpleGraph.Coloring.valid`
`mono` 📖	mathematical	—	`SimpleGraph.Colorable`	—	`Fintype.card_fin`
`mono_left` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`SimpleGraph.Colorable`	—	—
`of_embedding` 📖	mathematical	—	`SimpleGraph.Colorable`	—	`of_hom`
`of_hom` 📖	mathematical	—	`SimpleGraph.Colorable`	—	`Fintype.card_fin`
`of_isEmpty` 📖	mathematical	—	`SimpleGraph.Colorable`	—	—

SimpleGraph.Coloring

Definitions

Name	Category	Theorems
`colorClass` 📖	CompOp	3 math math: `mem_colorClass`, `color_classes_independent`, `mem_colorClasses`
`colorClasses` 📖	CompOp	5 math math: `colorClasses_finite`, `card_colorClasses_le`, `colorClasses_isPartition`, `toPartition_parts`, `mem_colorClasses`
`mk` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_colorClasses_le` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Set` `colorClasses`	—	`Setoid.card_classes_ker_le`
`colorClasses_finite` 📖	mathematical	—	`Set.Finite` `Set` `colorClasses`	—	`Setoid.finite_classes_ker`
`colorClasses_isPartition` 📖	mathematical	—	`Setoid.IsPartition` `colorClasses`	—	`Setoid.isPartition_classes`
`color_classes_independent` 📖	mathematical	—	`IsAntichain` `SimpleGraph.Adj` `colorClass`	—	`not_adj_of_mem_colorClass`
`colorable` 📖	mathematical	—	`SimpleGraph.Colorable` `Fintype.card`	—	`Fintype.card_fin`
`injective_comp_of_pairwise_adj` 📖	mathematical	`Pairwise` `SimpleGraph.Adj`	`DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.completeGraph`	—	`Function.injective_iff_pairwise_ne` `Pairwise.mono` `valid`
`mem_colorClass` 📖	mathematical	—	`Set` `Set.instMembership` `colorClass` `DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.completeGraph`	—	—
`mem_colorClasses` 📖	mathematical	—	`Set` `Set.instMembership` `colorClasses` `colorClass` `DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.completeGraph`	—	—
`not_adj_of_mem_colorClass` 📖	mathematical	`Set` `Set.instMembership` `colorClass`	`SimpleGraph.Adj`	—	`valid`
`surjOn_of_card_le_isClique` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike` `Fintype.card` `Finset.card`	`Set.SurjOn` `DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.completeGraph` `Set.univ`	—	`SimpleGraph.card_le_chromaticNumber_iff_forall_surjective` `SimpleGraph.chromaticNumber_top` `Fintype.card_coe` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Subtype.coe_prop`
`valid` 📖	—	`SimpleGraph.Adj`	—	—	`RelHom.map_rel`

SimpleGraph.CompleteBipartiteGraph

Definitions

Name	Category	Theorems
`bicoloring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chromaticNumber` 📖	mathematical	—	`SimpleGraph.chromaticNumber` `completeBipartiteGraph` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_two` `SimpleGraph.chromaticNumber_eq_iff_forall_surjective` `SimpleGraph.Coloring.colorable` `Fintype.card_fin` `Fintype.two_lt_card_iff` `SimpleGraph.Coloring.valid`

SimpleGraph.IsClique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_chromaticNumber` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `Finset.card` `SimpleGraph.chromaticNumber`	—	`SimpleGraph.le_chromaticNumber_of_pairwise_adj` `Nat.card_eq_fintype_card` `Fintype.card_coe`
`card_le_of_colorable` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card`	—	`Nat.card_eq_fintype_card` `Fintype.card_coe` `SimpleGraph.Colorable.card_le_of_pairwise_adj`
`card_le_of_coloring` 📖	mathematical	`SimpleGraph.IsClique` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `Fintype.card`	—	`card_le_of_colorable` `SimpleGraph.Coloring.colorable`

SimpleGraph.completeMultipartiteGraph

Definitions

Name	Category	Theorems
`coloring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chromaticNumber` 📖	mathematical	—	`SimpleGraph.chromaticNumber` `SimpleGraph.completeMultipartiteGraph` `ENat` `ENat.instNatCast` `Fintype.card`	—	`le_antisymm` `SimpleGraph.Colorable.chromaticNumber_le` `colorable` `not_cliqueFree_of_le_card` `le_rfl` `SimpleGraph.cliqueFree_of_chromaticNumber_lt`
`colorable` 📖	mathematical	—	`SimpleGraph.Colorable` `SimpleGraph.completeMultipartiteGraph` `Fintype.card`	—	`SimpleGraph.Coloring.colorable`
`colorable_of_cliqueFree` 📖	mathematical	`SimpleGraph.CliqueFree` `SimpleGraph.completeMultipartiteGraph`	`SimpleGraph.Colorable`	—	`SimpleGraph.not_cliqueFree_zero` `not_cliqueFree_of_infinite` `SimpleGraph.Colorable.mono` `SimpleGraph.Coloring.colorable` `not_cliqueFree_of_le_card` `le_rfl` `Mathlib.Tactic.Contrapose.contrapose₂` `SimpleGraph.CliqueFree.mono`

---

← Back to Index