Commit 2025-04-13 11:28 ff99cdae

View on Github →

feat(SimpleGraph/Walk): edge sets of walks (#23946) We introduce a definition SimpleGraph.Walk.edgeSet (p : SimpleGraph.Walk G u v) : Set (Sym2 V) for the edge set of a walk, and give a few very basic API lemmas. This allows us to avoid both decidability and the ugly p.edges.toFinset.toSet when talking about the set of edges of a walk.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.coe_edges_toFinset

added def SimpleGraph.Walk.edgeSet

added theorem SimpleGraph.Walk.edgeSet_append

added theorem SimpleGraph.Walk.edgeSet_concat

added theorem SimpleGraph.Walk.edgeSet_cons

added theorem SimpleGraph.Walk.edgeSet_copy

added theorem SimpleGraph.Walk.edgeSet_map

added theorem SimpleGraph.Walk.edgeSet_nil

added theorem SimpleGraph.Walk.edgeSet_reverse

added theorem SimpleGraph.Walk.edgeSet_transfer

added theorem SimpleGraph.Walk.mem_edgeSet