Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-26 22:13 8dd4619b

View on Github →

feat(combinatorics/simple_graph/connectivity): deleting edges outside a walk (#14110)

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.walk.is_path.to_delete_edges

added theorem simple_graph.walk.map_is_path_iff_of_injective

added theorem simple_graph.walk.map_to_delete_edges_eq

added def simple_graph.walk.to_delete_edge

added def simple_graph.walk.to_delete_edges