Commit 2026-06-05 15:27 7013b4ce

View on Github →

refactor(SimpleGraph): change bridges not to require the edge to be present (#32583) Remove the requirement for edges to exist in definition of isBridge, and then change the related lemmas to adjust for this, by renaming, fixing the statements and fixing the proofs, including in Acyclic. Closes #31690.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

modified theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge

deleted theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge

added theorem SimpleGraph.isAcyclic_iff_forall_isBridge

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

added theorem SimpleGraph.IsBridge.anti

deleted theorem SimpleGraph.IsBridge.anti_of_mem_edgeSet

added theorem SimpleGraph.IsBridge.notMem_edges_of_isCycle

modified theorem SimpleGraph.IsBridge.of_not_reachable

added theorem SimpleGraph.isBridge_deleteEdges_singleton

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges

added theorem SimpleGraph.isBridge_iff_forall_cycle_notMem

added theorem SimpleGraph.isBridge_iff_forall_walk_mem_edges

deleted theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem

added theorem SimpleGraph.isBridge_sup_edge

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

added theorem SimpleGraph.IsBridge.not_isEdgeReachable_two

deleted theorem SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two

added theorem SimpleGraph.isBridge_iff_not_isEdgeReachable_two

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

modified theorem SimpleGraph.deleteEdges_anti

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Star.lean