Documentation Verification Report

CompleteMultipartite

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

Statistics

Metric	Count
Definitions `CompleteEquipartiteSubgraph`, `ofCopy`, `parts`, `toCopy`, `verts`, `IsCompleteMultipartite`, `iso`, `setoid`, `IsPathGraph3Compl`, `pathGraph3ComplEmbedding`, `completeEquipartiteGraph`, `completeMultipartiteGraph`, `turanGraph`, `pathGraph3ComplEmbeddingOf`	14
Theorems `card_mem_parts`, `card_parts`, `card_verts`, `disjoint`, `ext`, `ext_iff`, `isCompleteBetween`, `nonempty_of_eq_zero_or_eq_zero`, `verts_eq_biUnion`, `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`, `completeEquipartiteGraph_isContained_iff`, `completeEquipartiteGraph_succ_isContained_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`	33
Total	47

SimpleGraph

Definitions

Name	Category	Theorems
`CompleteEquipartiteSubgraph` 📖	CompData	3 math math: `completeEquipartiteGraph_isContained_iff`, `CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero`, `completeEquipartiteGraph_succ_isContained_iff`
`IsCompleteMultipartite` 📖	MathDef	8 math math: `not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`, `colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree`, `IsCompleteMultipartite.comap`, `bot_isCompleteMultipartite`, `not_isCompleteMultipartite_of_pathGraph3ComplEmbedding`, `completeMultipartiteGraph.isCompleteMultipartite`, `completeEquipartiteGraph.isCompleteMultipartite`, `isCompleteMultipartite_iff`
`IsPathGraph3Compl` 📖	CompData	4 math math: `IsPathGraph3Compl.symm`, `not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`, `exists_isPathGraph3Compl_of_not_isCompleteMultipartite`, `IsFiveWheelLike.isPathGraph3Compl`
`completeEquipartiteGraph` 📖	CompOp	11 math math: `completeEquipartiteGraph_colorable`, `completeEquipartiteGraph_isContained_iff`, `isContained_completeEquipartiteGraph_of_colorable`, `neighborFinset_completeEquipartiteGraph`, `degree_completeEquipartiteGraph`, `completeEquipartiteGraph_adj`, `completeEquipartiteGraph_succ_isContained_iff`, `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.toPow` `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`
`completeEquipartiteGraph_isContained_iff` 📖	mathematical	—	`IsContained` `completeEquipartiteGraph` `CompleteEquipartiteSubgraph`	—	—
`completeEquipartiteGraph_succ_isContained_iff` 📖	mathematical	—	`IsContained` `completeEquipartiteGraph` `CompleteEquipartiteSubgraph` `Finset` `Finset.card` `IsCompleteBetween` `SetLike.coe` `Finset.instSetLike`	—	`completeEquipartiteGraph_eq_bot_iff` `instIsEmptyFalse` `CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero` `completeEquipartiteGraph_isContained_iff` `Finset.exists_subset_card_eq` `CompleteEquipartiteSubgraph.card_parts` `CompleteEquipartiteSubgraph.card_mem_parts` `CompleteEquipartiteSubgraph.isCompleteBetween` `Finset.exists_eq_insert_iff` `Finset.card_pos` `loopless` `Finset.card_cons` `Finset.coe_cons` `Set.Pairwise.insert_of_symmetric` `IsCompleteBetween.symm`
`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` `adj_comm`
`isCompleteMultipartite_iff` 📖	mathematical	—	`IsCompleteMultipartite` `Iso` `completeMultipartiteGraph`	—	`RelIso.map_rel_iff` `IsTrans.trans` `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` `IsTrans.trans` `adj_comm`
`not_isCompleteMultipartite_of_pathGraph3ComplEmbedding` 📖	mathematical	—	`IsCompleteMultipartite`	—	`Fin.instNeZeroHAddNatOfNat_mathlib_1` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `IsTrans.trans`

SimpleGraph.CompleteEquipartiteSubgraph

Definitions

Name	Category	Theorems
`ofCopy` 📖	CompOp	—
`parts` 📖	CompOp	5 math math: `isCompleteBetween`, `disjoint`, `card_parts`, `verts_eq_biUnion`, `ext_iff`
`toCopy` 📖	CompOp	—
`verts` 📖	CompOp	2 math math: `verts_eq_biUnion`, `card_verts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_mem_parts` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `parts`	`Finset.card`	—	—
`card_parts` 📖	mathematical	—	`Finset.card` `Finset` `parts`	—	—
`card_verts` 📖	mathematical	—	`Finset.card` `verts`	—	`disjoint` `Finset.card_disjiUnion` `Finset.sum_congr` `card_mem_parts` `Finset.sum_const` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `card_parts`
`disjoint` 📖	mathematical	—	`Set.Pairwise` `Finset` `SetLike.coe` `Finset.instSetLike` `parts` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot`	—	`Finset.disjoint_left` `SimpleGraph.loopless` `isCompleteBetween`
`ext` 📖	—	`parts`	—	—	—
`ext_iff` 📖	mathematical	—	`parts`	—	`ext`
`isCompleteBetween` 📖	mathematical	—	`Set.Pairwise` `Finset` `SetLike.coe` `Finset.instSetLike` `parts` `SimpleGraph.IsCompleteBetween`	—	—
`nonempty_of_eq_zero_or_eq_zero` 📖	mathematical	—	`SimpleGraph.CompleteEquipartiteSubgraph`	—	`instIsEmptyFalse` `Finset.coe_empty`
`verts_eq_biUnion` 📖	mathematical	—	`verts` `Finset.biUnion` `Finset` `parts`	—	`disjoint` `verts.eq_1` `Finset.disjiUnion_eq_biUnion`

SimpleGraph.IsCompleteMultipartite

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colorable_of_cliqueFree` 📖	mathematical	`SimpleGraph.CliqueFree`	`SimpleGraph.Colorable`	—	`SimpleGraph.Colorable.of_hom` `SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree` `SimpleGraph.CliqueFree.comap`
`comap` 📖	mathematical	—	`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