Commit 2025-08-19 06:18 0f16edbb

View on Github →

feat(SimpleGraph): sub-walks (#26655) defines (contiguous) subwalks and provides lemmas about them.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.isPath_of_isSubwalk

added theorem SimpleGraph.Walk.isTrail_of_isSubwalk

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.IsSubwalk.trans

added def SimpleGraph.Walk.IsSubwalk

added theorem SimpleGraph.Walk.drop_support_eq_support_drop_min

added theorem SimpleGraph.Walk.drop_zero

added theorem SimpleGraph.Walk.isSubwalk_antisymm

added theorem SimpleGraph.Walk.isSubwalk_cons

added theorem SimpleGraph.Walk.isSubwalk_iff_support_isInfix

added theorem SimpleGraph.Walk.isSubwalk_nil_iff

added theorem SimpleGraph.Walk.isSubwalk_of_append_left

added theorem SimpleGraph.Walk.isSubwalk_of_append_right

added theorem SimpleGraph.Walk.isSubwalk_rfl

added theorem SimpleGraph.Walk.length_le_of_isSubwalk

added theorem SimpleGraph.Walk.nil_isSubwalk

added theorem SimpleGraph.Walk.nil_isSubwalk_iff_exists

added theorem SimpleGraph.Walk.support_append_eq_support_dropLast_append

added theorem SimpleGraph.Walk.take_support_eq_support_take_succ

Modified Mathlib/Data/List/Infix.lean

added theorem List.infix_antisymm

added theorem List.infix_singleton_iff

added theorem List.prefix_append_drop

added theorem List.singleton_infix_iff

added theorem List.singleton_infix_singleton_iff