Commit 2025-12-26 18:30 8825dc85

View on Github →

feat(Combinatorics/SimpleGraph): define edge-connectivity (#32870) This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691.

Estimated changes

Modified Mathlib.lean

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

added theorem SimpleGraph.IsEdgeConnected.connected

added theorem SimpleGraph.IsEdgeConnected.preconnected

added def SimpleGraph.IsEdgeConnected

added theorem SimpleGraph.IsEdgeReachable.anti

added theorem SimpleGraph.IsEdgeReachable.mono

added theorem SimpleGraph.IsEdgeReachable.reachable

added theorem SimpleGraph.IsEdgeReachable.rfl

added theorem SimpleGraph.IsEdgeReachable.symm

added theorem SimpleGraph.IsEdgeReachable.trans

added def SimpleGraph.IsEdgeReachable

added theorem SimpleGraph.isBridge_iff_adj_and_not_isEdgeConnected_two

added theorem SimpleGraph.isEdgeConnected_add_one

added theorem SimpleGraph.isEdgeConnected_one

added theorem SimpleGraph.isEdgeConnected_two

added theorem SimpleGraph.isEdgeReachable_add_one

added theorem SimpleGraph.isEdgeReachable_one