Commit 2025-11-20 13:23 1bf88df8

View on Github →

feat(Combinatorics/SimpleGraph/Walk): a vertex is in the support iff an edge in the walk contains it (#31678)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.mem_support_iff_exists_mem_edges

added theorem SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil

added theorem SimpleGraph.Walk.mem_support_of_mem_edges