Commit 2025-12-10 18:38 fa9f474c

View on Github →

feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges (#31416)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

modified theorem SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edges

modified theorem SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges

Modified Mathlib/Combinatorics/SimpleGraph/Walks/Basic.lean

added theorem SimpleGraph.Walk.darts_eq_nil

added theorem SimpleGraph.Walk.edges_eq_nil

deleted theorem SimpleGraph.Walk.getLast_darts_snd

deleted theorem SimpleGraph.Walk.head_darts_fst

Modified Mathlib/Combinatorics/SimpleGraph/Walks/Traversal.lean

added theorem SimpleGraph.Walk.firstDart_eq_head_darts

added theorem SimpleGraph.Walk.firstDart_mem_darts

added theorem SimpleGraph.Walk.getLast_darts_eq_lastDart

added theorem SimpleGraph.Walk.getLast_darts_snd

added theorem SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end

added theorem SimpleGraph.Walk.head_darts_eq_firstDart

added theorem SimpleGraph.Walk.head_darts_fst

added theorem SimpleGraph.Walk.head_edges_eq_mk_start_snd

added theorem SimpleGraph.Walk.lastDart_eq_getLast_darts

added theorem SimpleGraph.Walk.lastDart_mem_darts

added theorem SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges

added theorem SimpleGraph.Walk.mk_penultimate_end_mem_edges

added theorem SimpleGraph.Walk.mk_start_snd_eq_head_edges

added theorem SimpleGraph.Walk.mk_start_snd_mem_edges

added theorem SimpleGraph.Walk.penultimate_mem_dropLast_support

added theorem SimpleGraph.Walk.snd_eq_support_getElem_one

added theorem SimpleGraph.Walk.support_getElem_eq_getVert

added theorem SimpleGraph.Walk.support_getElem_length_sub_one_eq_penultimate

added theorem SimpleGraph.Walk.support_getElem_one