Commit 2025-11-04 05:46 02e7537e

View on Github →

feat(Combinatorics/SimpleGraph/Walk): mapLe preservation lemmas (#30602) feat(Combinatorics/SimpleGraph/Walk): specialize map preservation lemmas from for mapLe

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.edgeSet_mapLe_eq_edgeSet

added theorem SimpleGraph.Walk.edges_mapLe_eq_edges

added theorem SimpleGraph.Walk.support_mapLe_eq_support