Documentation Verification Report

CompleteMultipartite

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

Statistics

Metric	Count
Definitions `IsCompleteMultipartite`, `iso`, `setoid`, `IsPathGraph3Compl`, `pathGraph3ComplEmbedding`, `completeEquipartiteGraph`, `completeMultipartiteGraph`, `turanGraph`, `pathGraph3ComplEmbeddingOf`	9
Theorems `colorable_of_cliqueFree`, `comap`, `adj`, `fst_ne_snd`, `ne_fst`, `ne_snd`, `not_adj_fst`, `not_adj_snd`, `bot_isCompleteMultipartite`, `card_edgeFinset_completeEquipartiteGraph`, `isCompleteMultipartite`, `completeEquipartiteGraph_adj`, `completeEquipartiteGraph_eq_bot_iff`, `isCompleteMultipartite`, `degree_completeEquipartiteGraph`, `exists_isPathGraph3Compl_of_not_isCompleteMultipartite`, `isCompleteMultipartite_iff`, `isContained_completeEquipartiteGraph_of_colorable`, `neighborFinset_completeEquipartiteGraph`, `neighborSet_completeEquipartiteGraph`, `not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`, `not_isCompleteMultipartite_of_pathGraph3ComplEmbedding`	22
Total	31

SimpleGraph

Definitions

Name	Category	Theorems
`IsCompleteMultipartite` 📖	MathDef	7 math math: `not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`, `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree`, `bot_isCompleteMultipartite`, `not_isCompleteMultipartite_of_pathGraph3ComplEmbedding`, `completeMultipartiteGraph.isCompleteMultipartite`, `completeEquipartiteGraph.isCompleteMultipartite`, `isCompleteMultipartite_iff`
`IsPathGraph3Compl` 📖	CompData	3 math math: `not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`, `exists_isPathGraph3Compl_of_not_isCompleteMultipartite`, `IsFiveWheelLike.isPathGraph3Compl`
`completeEquipartiteGraph` 📖	CompOp	9 math math: `completeEquipartiteGraph_colorable`, `isContained_completeEquipartiteGraph_of_colorable`, `neighborFinset_completeEquipartiteGraph`, `degree_completeEquipartiteGraph`, `completeEquipartiteGraph_adj`, `completeEquipartiteGraph_eq_bot_iff`, `card_edgeFinset_completeEquipartiteGraph`, `completeEquipartiteGraph.isCompleteMultipartite`, `neighborSet_completeEquipartiteGraph`
`pathGraph3ComplEmbeddingOf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_isCompleteMultipartite` 📖	mathematical	—	`IsCompleteMultipartite` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`card_edgeFinset_completeEquipartiteGraph` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `completeEquipartiteGraph` `fintypeEdgeSet` `Sym2.instFintype` `instFintypeProd` `Fin.fintype` `instDecidableComapAdj` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.adjDecidable` `Nat.choose` `Monoid.toNatPow` `Nat.instMonoid`	—	`mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `two_ne_zero` `sum_degrees_eq_twice_card_edges` `degree_completeEquipartiteGraph` `Finset.sum_const` `smul_eq_mul` `Finset.card_univ` `Fintype.card_prod` `Fintype.card_fin` `Nat.choose_two_right` `Nat.instAtLeastTwoHAddOfNat` `Even.two_dvd` `Nat.even_mul_pred_self` `mul_assoc` `mul_comm` `pow_two`
`completeEquipartiteGraph_adj` 📖	mathematical	—	`Adj` `completeEquipartiteGraph`	—	—
`completeEquipartiteGraph_eq_bot_iff` 📖	mathematical	—	`completeEquipartiteGraph` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `edgeSet_nonempty` `Fin.nontrivial_iff_two_le` `Sym2.ind` `completeEquipartiteGraph_adj` `mem_edgeSet`
`degree_completeEquipartiteGraph` 📖	mathematical	—	`degree` `completeEquipartiteGraph` `neighborSetFintype` `instFintypeProd` `Fin.fintype` `instDecidableComapAdj` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.adjDecidable`	—	`card_neighborFinset_eq_degree` `neighborFinset_completeEquipartiteGraph` `Finset.card_product` `Finset.card_compl` `Finset.card_singleton` `Fintype.card_fin` `Finset.card_univ`
`exists_isPathGraph3Compl_of_not_isCompleteMultipartite` 📖	mathematical	`IsCompleteMultipartite`	`IsPathGraph3Compl`	—	`Mathlib.Tactic.Push.not_forall_eq` `Transitive.eq_1` `IsCompleteMultipartite.eq_1` `adj_comm`
`isCompleteMultipartite_iff` 📖	mathematical	—	`IsCompleteMultipartite` `Iso` `completeMultipartiteGraph`	—	`RelIso.map_rel_iff` `completeMultipartiteGraph.isCompleteMultipartite`
`isContained_completeEquipartiteGraph_of_colorable` 📖	mathematical	`Fintype.card` `Set.Elem` `Coloring.colorClass` `Subtype.fintype` `Set` `Set.instMembership` `instDecidablePredMemSetColorClassOfDecidableEq`	`IsContained` `completeEquipartiteGraph`	—	`Function.Embedding.nonempty_iff_card_le` `Fintype.card_fin` `congr_heq` `Subtype.heq_iff_coe_eq` `Function.Embedding.injective` `Coloring.mem_colorClass` `Coloring.valid`
`neighborFinset_completeEquipartiteGraph` 📖	mathematical	—	`neighborFinset` `completeEquipartiteGraph` `neighborSetFintype` `instFintypeProd` `Fin.fintype` `instDecidableComapAdj` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.adjDecidable` `SProd.sprod` `Finset` `Finset.instSProd` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Finset.instSingleton` `Finset.univ`	—	`Finset.ext`
`neighborSet_completeEquipartiteGraph` 📖	mathematical	—	`neighborSet` `completeEquipartiteGraph` `SProd.sprod` `Set` `Set.instSProd` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `Set.univ`	—	`Set.ext`
`not_isCompleteMultipartite_iff_exists_isPathGraph3Compl` 📖	mathematical	—	`IsCompleteMultipartite` `IsPathGraph3Compl`	—	`exists_isPathGraph3Compl_of_not_isCompleteMultipartite` `adj_comm`
`not_isCompleteMultipartite_of_pathGraph3ComplEmbedding` 📖	mathematical	—	`IsCompleteMultipartite`	—	`Fin.instNeZeroHAddNatOfNat_mathlib_1` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

SimpleGraph.IsCompleteMultipartite

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	—
`setoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colorable_of_cliqueFree` 📖	mathematical	`SimpleGraph.IsCompleteMultipartite` `SimpleGraph.CliqueFree`	`SimpleGraph.Colorable`	—	`SimpleGraph.Colorable.of_hom` `SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree` `SimpleGraph.CliqueFree.comap`
`comap` 📖	—	`SimpleGraph.IsCompleteMultipartite`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding`

SimpleGraph.IsPathGraph3Compl

Definitions

Name	Category	Theorems
`pathGraph3ComplEmbedding` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj` 📖	mathematical	`SimpleGraph.IsPathGraph3Compl`	`SimpleGraph.Adj`	—	—
`fst_ne_snd` 📖	—	`SimpleGraph.IsPathGraph3Compl`	—	—	`SimpleGraph.Adj.ne` `adj`
`ne_fst` 📖	—	`SimpleGraph.IsPathGraph3Compl`	—	—	`not_adj_snd` `adj`
`ne_snd` 📖	—	`SimpleGraph.IsPathGraph3Compl`	—	—	`not_adj_fst` `SimpleGraph.Adj.symm` `adj`
`not_adj_fst` 📖	mathematical	`SimpleGraph.IsPathGraph3Compl`	`SimpleGraph.Adj`	—	—
`not_adj_snd` 📖	mathematical	`SimpleGraph.IsPathGraph3Compl`	`SimpleGraph.Adj`	—	—

SimpleGraph.completeEquipartiteGraph

Definitions

Name	Category	Theorems
`completeMultipartiteGraph` 📖	CompOp	—
`turanGraph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompleteMultipartite` 📖	mathematical	—	`SimpleGraph.IsCompleteMultipartite` `SimpleGraph.completeEquipartiteGraph`	—	`SimpleGraph.completeEquipartiteGraph_eq_bot_iff` `SimpleGraph.bot_isCompleteMultipartite` `SimpleGraph.isCompleteMultipartite_iff`

SimpleGraph.completeMultipartiteGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompleteMultipartite` 📖	mathematical	—	`SimpleGraph.IsCompleteMultipartite` `SimpleGraph.completeMultipartiteGraph`	—	—

---

← Back to Index