Documentation Verification Report

Sum

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

Statistics

Metric	Count
Definitions `sum`, `sumEquiv`, `sumFin`, `sumLeft`, `sumRight`, `sumInl`, `sumInr`, `sumAssoc`, `sumComm`, `sum`, `«term_⊕g_»`	11
Theorems `of_sum_left`, `of_sum_right`, `sum_max`, `sumLeft_sum`, `sumRight_sum`, `sum_sumLeft_sumRight`, `sum_sup_edge`, `sumInl_apply`, `sumInr_apply`, `sumAssoc_apply`, `sumAssoc_symm_apply`, `sumComm_apply`, `sumComm_symm_apply`, `sum_sup_edge`, `sum_sup_edge`, `chromaticNumber_le_sum_left`, `chromaticNumber_le_sum_right`, `chromaticNumber_sum`, `colorable_sum`, `sum_adj`	20
Total	31

SimpleGraph

Definitions

Name	Category	Theorems
`sum` 📖	CompOp	21 math math: `sum_adj`, `Embedding.sumInr_apply`, `Iso.sumComm_apply`, `chromaticNumber_le_sum_right`, `Iso.sumBoxProdDistrib_apply`, `Embedding.sumInl_apply`, `chromaticNumber_sum`, `colorable_sum`, `Colorable.sum_max`, `Reachable.sum_sup_edge`, `Iso.boxProdSumDistrib_symm_apply`, `Iso.boxProdSumDistrib_apply`, `Iso.boxProdSumDistrib_toEquiv`, `chromaticNumber_le_sum_left`, `Iso.sumAssoc_apply`, `Preconnected.sum_sup_edge`, `Iso.sumBoxProdDistrib_symm_apply`, `Iso.sumAssoc_symm_apply`, `Iso.sumBoxProdDistrib_toEquiv`, `Iso.sumComm_symm_apply`, `Connected.sum_sup_edge`
`«term_⊕g_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chromaticNumber_le_sum_left` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `sum`	—	`chromaticNumber_le_of_forall_imp` `Colorable.of_sum_left`
`chromaticNumber_le_sum_right` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `sum`	—	`chromaticNumber_le_of_forall_imp` `Colorable.of_sum_right`
`chromaticNumber_sum` 📖	mathematical	—	`chromaticNumber` `sum` `ENat` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`eq_max` `chromaticNumber_le_sum_left` `chromaticNumber_le_sum_right` `chromaticNumber_le_iff_colorable`
`colorable_sum` 📖	mathematical	—	`Colorable` `sum`	—	`Colorable.of_sum_left` `Colorable.of_sum_right` `Colorable.sum_max`
`sum_adj` 📖	mathematical	—	`Adj` `sum`	—	—

SimpleGraph.Colorable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_sum_left` 📖	mathematical	—	`SimpleGraph.Colorable`	—	—
`of_sum_right` 📖	mathematical	—	`SimpleGraph.Colorable`	—	—
`sum_max` 📖	mathematical	—	`SimpleGraph.Colorable` `SimpleGraph.sum`	—	—

SimpleGraph.Coloring

Definitions

Name	Category	Theorems
`sum` 📖	CompOp	3 math math: `sumRight_sum`, `sumLeft_sum`, `sum_sumLeft_sumRight`
`sumEquiv` 📖	CompOp	—
`sumFin` 📖	CompOp	—
`sumLeft` 📖	CompOp	2 math math: `sumLeft_sum`, `sum_sumLeft_sumRight`
`sumRight` 📖	CompOp	2 math math: `sumRight_sum`, `sum_sumLeft_sumRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumLeft_sum` 📖	mathematical	—	`sumLeft` `sum`	—	—
`sumRight_sum` 📖	mathematical	—	`sumRight` `sum`	—	—
`sum_sumLeft_sumRight` 📖	mathematical	—	`sum` `sumLeft` `sumRight`	—	`RelHom.ext`

SimpleGraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_sup_edge` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sum` `SimpleGraph.edge`	—	`SimpleGraph.Preconnected.sum_sup_edge` `preconnected`

SimpleGraph.Embedding

Definitions

Name	Category	Theorems
`sumInl` 📖	CompOp	1 math math: `sumInl_apply`
`sumInr` 📖	CompOp	1 math math: `sumInr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumInl_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `SimpleGraph.Adj` `SimpleGraph.sum` `RelEmbedding.instFunLike` `sumInl`	—	—
`sumInr_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `SimpleGraph.Adj` `SimpleGraph.sum` `RelEmbedding.instFunLike` `sumInr`	—	—

SimpleGraph.Iso

Definitions

Name	Category	Theorems
`sumAssoc` 📖	CompOp	2 math math: `sumAssoc_apply`, `sumAssoc_symm_apply`
`sumComm` 📖	CompOp	2 math math: `sumComm_apply`, `sumComm_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `RelIso.instFunLike` `sumAssoc`	—	—
`sumAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `RelIso.instFunLike` `RelIso.symm` `sumAssoc`	—	—
`sumComm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `RelIso.instFunLike` `sumComm`	—	—
`sumComm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `RelIso.instFunLike` `RelIso.symm` `sumComm`	—	—

SimpleGraph.Preconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_sup_edge` 📖	mathematical	`SimpleGraph.Preconnected`	`SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sum` `SimpleGraph.edge`	—	`SimpleGraph.Reachable.mono` `le_sup_left` `SimpleGraph.Reachable.map` `SimpleGraph.Reachable.sum_sup_edge` `SimpleGraph.Reachable.symm`

SimpleGraph.Reachable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_sup_edge` 📖	mathematical	—	`SimpleGraph.Reachable` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sum` `SimpleGraph.edge`	—	`trans` `mono` `le_sup_left` `map` `symm` `SimpleGraph.Adj.reachable` `SimpleGraph.sum_adj`

---

← Back to Index