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.