Arborescence

📁 Source: Mathlib/Combinatorics/Quiver/Arborescence.lean

Statistics

Metric	Count
Definitions Arborescence, root, uniquePath, RootedConnected, arborescenceMk, geodesicArborescence, geodesicSubtree, instUniquePathRoot, root, shortestPath	10
Theorems nonempty_path, shortest_path_spec	2
Total	12

Quiver

Definitions

Name	Category	Theorems
Arborescence 📖	CompData	—
RootedConnected 📖	CompData	1 math math: IsFreeGroupoid.generators_connected
arborescenceMk 📖	CompOp	—
geodesicArborescence 📖	CompOp	—
geodesicSubtree 📖	CompOp	—
instUniquePathRoot 📖	CompOp	—
root 📖	CompOp	—
shortestPath 📖	CompOp	1 math math: shortest_path_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shortest_path_spec 📖	mathematical	—	Path.length shortestPath	—	not_lt WellFounded.not_lt_min

Quiver.Arborescence

Definitions

Name	Category	Theorems
root 📖	CompOp	—
uniquePath 📖	CompOp	—

Quiver.RootedConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_path 📖	mathematical	—	Quiver.Path	—	—

---

← Back to Index