Documentation Verification Report

LineGraph

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

Statistics

Metric	Count
Definitions `lineGraph`, `toLineGraphEmbedding`, `lineGraph`, `lineGraph`	4
Theorems `isIndContained_lineGraph`, `lineGraph`, `lineGraph`, `lineGraph`, `lineGraph_adj_iff_exists`, `lineGraph_bot`, `map_lineGraph_le_of_le`	7
Total	11

SimpleGraph

Definitions

Name	Category	Theorems
`lineGraph` 📖	CompOp	7 math math: `IsSubgraph.lineGraph`, `map_lineGraph_le_of_le`, `IsContained.isIndContained_lineGraph`, `IsIndContained.lineGraph`, `lineGraph_bot`, `IsContained.lineGraph`, `lineGraph_adj_iff_exists`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineGraph_adj_iff_exists` 📖	mathematical	—	`Adj` `Set.Elem` `Sym2` `edgeSet` `lineGraph` `SetLike.instMembership` `Sym2.instSetLike` `Set` `Set.instMembership`	—	—
`lineGraph_bot` 📖	mathematical	—	`lineGraph` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Set.Elem` `Sym2` `edgeSet`	—	`ext` `edgeSet_bot`
`map_lineGraph_le_of_le` 📖	mathematical	`SimpleGraph` `instLE`	`SimpleGraph` `Sym2` `instLE` `map` `Set` `Set.instMembership` `edgeSet` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.subtype` `lineGraph`	—	—

SimpleGraph.Copy

Definitions

Name	Category	Theorems
`lineGraph` 📖	CompOp	—
`toLineGraphEmbedding` 📖	CompOp	—

SimpleGraph.IsContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIndContained_lineGraph` 📖	mathematical	—	`SimpleGraph.IsIndContained` `Set.Elem` `Sym2` `SimpleGraph.edgeSet` `SimpleGraph.lineGraph`	—	—
`lineGraph` 📖	mathematical	—	`SimpleGraph.IsContained` `Set.Elem` `Sym2` `SimpleGraph.edgeSet` `SimpleGraph.lineGraph`	—	—

SimpleGraph.IsIndContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineGraph` 📖	mathematical	—	`SimpleGraph.IsIndContained` `Set.Elem` `Sym2` `SimpleGraph.edgeSet` `SimpleGraph.lineGraph`	—	—

SimpleGraph.IsSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lineGraph` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`SimpleGraph` `Sym2` `SimpleGraph.instLE` `SimpleGraph.map` `Set` `Set.instMembership` `SimpleGraph.edgeSet` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.subtype` `SimpleGraph.lineGraph`	—	`SimpleGraph.map_lineGraph_le_of_le`

SimpleGraph.Iso

Definitions

Name	Category	Theorems
`lineGraph` 📖	CompOp	—

---

← Back to Index