Commit 2026-08-04 16:19 98d2c1d1

View on Github →

feat(SimpleGraph/Walk/Operations): more operations API (#41460) Tags Hom.ofLE as @[implicit_reducible] to let rw/simp use map API on mapLe.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean

modified theorem SimpleGraph.Walk.edgeSet_mapLe_eq_edgeSet

modified theorem SimpleGraph.Walk.edges_mapLe_eq_edges

added theorem SimpleGraph.Walk.length_mapLe

added theorem SimpleGraph.Walk.mapLe_append

added theorem SimpleGraph.Walk.reverse_mapLe

modified theorem SimpleGraph.Walk.support_mapLe_eq_support

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

modified theorem SimpleGraph.Walk.cons_support_tail

added theorem SimpleGraph.Walk.darts_dropLast

added theorem SimpleGraph.Walk.darts_tail

added theorem SimpleGraph.Walk.drop_drop

added theorem SimpleGraph.Walk.edges_dropLast

added theorem SimpleGraph.Walk.edges_tail

added theorem SimpleGraph.Walk.getVert_append'

added theorem SimpleGraph.Walk.getVert_dropLast

added theorem SimpleGraph.Walk.length_tail

modified theorem SimpleGraph.Walk.length_tail_add_one

added theorem SimpleGraph.Walk.reverse_dropLast

added theorem SimpleGraph.Walk.reverse_tail