LineGraph

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

Statistics

Metric	Count
Definitions lineGraph	1
Theorems lineGraph_adj_iff_exists, lineGraph_bot	2
Total	3

SimpleGraph

Definitions

Name	Category	Theorems
lineGraph 📖	CompOp	2 math math: lineGraph_bot, 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

---

← Back to Index