Documentation Verification Report

EdgeLabeling

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

Statistics

Metric	Count
Definitions `EdgeLabeling`, `compRight`, `get`, `instDecidableRelAdjLabelGraphOfDecidableEq`, `labelGraph`, `mk`, `pullback`, `TopEdgeLabeling`, `pullback`, `instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet`, `instInhabitedEdgeLabeling`, `instUniqueEdgeLabeling`, `toTopEdgeLabeling`	13
Theorems `compRight_apply`, `compRight_get`, `ext_get`, `ext_get_iff`, `get_comm`, `get_eq`, `get_mk`, `get_pullback`, `iSup_labelGraph`, `labelGraph_adj`, `labelGraph_le`, `pairwiseDisjoint_univ_labelGraph`, `pairwise_disjoint_labelGraph`, `pullback_apply`, `labelGraph_adj`, `labelGraph_toTopEdgeLabeling`, `card_topEdgeLabeling`, `instFiniteEdgeLabelingOfElemSym2EdgeSet`, `instNonemptyEdgeLabeling`, `instNontrivialEdgeLabelingOfNonemptyElemSym2EdgeSet`, `instSubsingletonEdgeLabeling`, `toTopEdgeLabeling_get`, `toTopEdgeLabeling_labelGraph`, `toTopEdgeLabeling_labelGraph_compl`	24
Total	37

SimpleGraph

Definitions

Name	Category	Theorems
`EdgeLabeling` 📖	CompOp	4 math math: `instNonemptyEdgeLabeling`, `instNontrivialEdgeLabelingOfNonemptyElemSym2EdgeSet`, `instFiniteEdgeLabelingOfElemSym2EdgeSet`, `instSubsingletonEdgeLabeling`
`TopEdgeLabeling` 📖	CompOp	1 math math: `card_topEdgeLabeling`
`instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet` 📖	CompOp	1 math math: `card_topEdgeLabeling`
`instInhabitedEdgeLabeling` 📖	CompOp	—
`instUniqueEdgeLabeling` 📖	CompOp	—
`toTopEdgeLabeling` 📖	CompOp	4 math math: `toTopEdgeLabeling_labelGraph_compl`, `toTopEdgeLabeling_get`, `toTopEdgeLabeling_labelGraph`, `TopEdgeLabeling.labelGraph_toTopEdgeLabeling`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_topEdgeLabeling` 📖	mathematical	—	`Fintype.card` `TopEdgeLabeling` `instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `fintypeEdgeSet` `Sym2.instFintype` `Top.adjDecidable` `Monoid.toNatPow` `Nat.instMonoid` `Nat.choose`	—	`Fintype.card_fun` `edgeFinset_card` `card_edgeFinset_top_eq_card_choose_two`
`instFiniteEdgeLabelingOfElemSym2EdgeSet` 📖	mathematical	—	`Finite` `EdgeLabeling`	—	`Pi.finite`
`instNonemptyEdgeLabeling` 📖	mathematical	—	`EdgeLabeling`	—	—
`instNontrivialEdgeLabelingOfNonemptyElemSym2EdgeSet` 📖	mathematical	—	`Nontrivial` `EdgeLabeling`	—	`Function.nontrivial`
`instSubsingletonEdgeLabeling` 📖	mathematical	—	`EdgeLabeling`	—	—
`toTopEdgeLabeling_get` 📖	mathematical	—	`EdgeLabeling.get` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `toTopEdgeLabeling` `Adj`	—	—
`toTopEdgeLabeling_labelGraph` 📖	mathematical	—	`EdgeLabeling.labelGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `toTopEdgeLabeling`	—	`ext` `ne_of_adj`
`toTopEdgeLabeling_labelGraph_compl` 📖	mathematical	—	`EdgeLabeling.labelGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `toTopEdgeLabeling` `Compl.compl` `instCompl`	—	`ext`

SimpleGraph.EdgeLabeling

Definitions

Name	Category	Theorems
`compRight` 📖	CompOp	2 math math: `compRight_get`, `compRight_apply`
`get` 📖	CompOp	8 math math: `compRight_get`, `SimpleGraph.TopEdgeLabeling.labelGraph_adj`, `get_comm`, `get_pullback`, `SimpleGraph.toTopEdgeLabeling_get`, `get_mk`, `ext_get_iff`, `get_eq`
`instDecidableRelAdjLabelGraphOfDecidableEq` 📖	CompOp	1 math math: `SimpleGraph.TopEdgeLabeling.labelGraph_toTopEdgeLabeling`
`labelGraph` 📖	CompOp	9 math math: `SimpleGraph.TopEdgeLabeling.labelGraph_adj`, `SimpleGraph.toTopEdgeLabeling_labelGraph_compl`, `labelGraph_le`, `iSup_labelGraph`, `pairwise_disjoint_labelGraph`, `SimpleGraph.toTopEdgeLabeling_labelGraph`, `pairwiseDisjoint_univ_labelGraph`, `SimpleGraph.TopEdgeLabeling.labelGraph_toTopEdgeLabeling`, `labelGraph_adj`
`mk` 📖	CompOp	—
`pullback` 📖	CompOp	2 math math: `pullback_apply`, `get_pullback`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRight_apply` 📖	mathematical	—	`compRight`	—	—
`compRight_get` 📖	mathematical	`SimpleGraph.Adj`	`get` `compRight`	—	—
`ext_get` 📖	—	`get`	—	—	`Sym2.inductionOn`
`ext_get_iff` 📖	mathematical	—	`get`	—	`ext_get`
`get_comm` 📖	mathematical	`SimpleGraph.Adj`	`get` `SimpleGraph.Adj.symm`	—	`SimpleGraph.Adj.symm` `Sym2.eq_swap`
`get_eq` 📖	mathematical	`SimpleGraph.Adj`	`get` `Sym2` `Set` `Set.instMembership` `SimpleGraph.edgeSet`	—	—
`get_mk` 📖	mathematical	`SimpleGraph.Adj.symm` `SimpleGraph.Adj`	`get`	—	`SimpleGraph.Adj.symm`
`get_pullback` 📖	mathematical	`SimpleGraph.Adj`	`get` `pullback` `RelEmbedding.toRelHom` `DFunLike.coe` `SimpleGraph.Embedding` `RelEmbedding.instFunLike`	—	—
`iSup_labelGraph` 📖	mathematical	—	`iSup` `SimpleGraph` `SimpleGraph.supSet` `labelGraph`	—	`SimpleGraph.ext`
`labelGraph_adj` 📖	mathematical	—	`SimpleGraph.Adj` `labelGraph` `Sym2` `Set` `Set.instMembership` `SimpleGraph.edgeSet`	—	`labelGraph.eq_1`
`labelGraph_le` 📖	mathematical	—	`SimpleGraph` `SimpleGraph.instLE` `labelGraph`	—	—
`pairwiseDisjoint_univ_labelGraph` 📖	mathematical	—	`Set.PairwiseDisjoint` `SimpleGraph` `SimpleGraph.instPartialOrder` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `Set.univ` `labelGraph`	—	`pairwise_disjoint_labelGraph`
`pairwise_disjoint_labelGraph` 📖	mathematical	—	`Pairwise` `Disjoint` `SimpleGraph` `SimpleGraph.instPartialOrder` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `labelGraph`	—	`SimpleGraph.disjoint_left`
`pullback_apply` 📖	mathematical	—	`pullback` `SimpleGraph.Hom.mapEdgeSet`	—	—

SimpleGraph.TopEdgeLabeling

Definitions

Name	Category	Theorems
`pullback` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`labelGraph_adj` 📖	mathematical	—	`SimpleGraph.Adj` `SimpleGraph.EdgeLabeling.labelGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `SimpleGraph.EdgeLabeling.get`	—	—
`labelGraph_toTopEdgeLabeling` 📖	mathematical	—	`SimpleGraph.toTopEdgeLabeling` `SimpleGraph.EdgeLabeling.labelGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `SimpleGraph.EdgeLabeling.instDecidableRelAdjLabelGraphOfDecidableEq` `SimpleGraph.Top.adjDecidable`	—	`SimpleGraph.EdgeLabeling.ext_get`

---

← Back to Index