Commit 2024-09-03 15:39 b8e23f0e
View on Github →feat(Combinatorics/SimpleGraph): darts and edges are injective for walks, length of paths and trails are bounded (#15541)
Provide theorems stating that SimpleGraph.Walk.darts and SimpleGraph.Walk.edges are injective functions, and that the length of SimpleGraph.Walk.IsTrail and SimpleGraph.Walk.IsPath is bounded for finite graphs.