Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 14:53 7a5f20f4

View on Github →

feat(combinatorics/simple_graph/connectivity): Transfer walks from a simple_graph to another (#17326)

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.walk.cons_is_cycle_iff

added theorem simple_graph.walk.edges_transfer

added theorem simple_graph.walk.reverse_transfer

added theorem simple_graph.walk.support_transfer

modified def simple_graph.walk.to_delete_edges

added def simple_graph.walk.transfer

added theorem simple_graph.walk.transfer_append

added theorem simple_graph.walk.transfer_eq_map_of_le

added theorem simple_graph.walk.transfer_is_cycle

added theorem simple_graph.walk.transfer_is_path

added theorem simple_graph.walk.transfer_self

added theorem simple_graph.walk.transfer_transfer