Theorem SimpleGraph.Connected.connected_delete_edge_of_not_isBridge

Modification history

2026-09-04 03:28
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
feat(SimpleGraph/Connectivity/Connected): deleting a non-bridge edge preserves reachability (#43055) …
Deleted SimpleGraph.Connected.connected_delete_edge_of_not_isBridgeView on Github →
2025-06-22 12:57
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
chore(SimpleGraph): split `Combinatorics.SimpleGraph.Path` (#25844) …
Modified SimpleGraph.Connected.connected_delete_edge_of_not_isBridgeView on Github →
2025-03-28 14:56
Mathlib/Combinatorics/SimpleGraph/Path.lean
feat(SimpleGraph): a connected graph with n - 1 edges is a tree (#23399) …
Added SimpleGraph.Connected.connected_delete_edge_of_not_isBridgeView on Github →