Theorem SimpleGraph.Walk.isSubwalk_nil_start

Modification history

2026-07-20 20:57
Mathlib/Combinatorics/SimpleGraph/Walk/Subwalks.lean
feat(SimpleGraph/Subwalks): an empty walk at `v` is a subwalk of any walk to `v` (#41626)
Added SimpleGraph.Walk.isSubwalk_nil_startView on Github →