Theorem SimpleGraph.Walk.isSubwalk_nil_end

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_endView on Github →