Commit 2026-09-04 03:28 2308bf95

View on Github →

feat(SimpleGraph/Connectivity/Connected): deleting a non-bridge edge preserves reachability (#43055) This generalizes an existing theorem about Connected to Preconnected and Reachable.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

deleted theorem SimpleGraph.Connected.connected_delete_edge_of_not_isBridge

added theorem SimpleGraph.Preconnected.connected_deleteEdges_of_not_isBridge

added theorem SimpleGraph.Reachable.reachable_deleteEdges_of_not_isBridge