Commit 2026-01-27 07:48 66892e66

View on Github →

feat(Combinatorics/SimpleGraph): more about two-reachability (#33335)

Estimated changes

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

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

added theorem SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_isEdgeReachable_two

modified theorem SimpleGraph.isEdgeConnected_two

modified theorem SimpleGraph.isEdgeReachable_add_one

added theorem SimpleGraph.isEdgeReachable_two

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

modified theorem SimpleGraph.deleteEdges_empty

added theorem SimpleGraph.deleteEdges_of_subset_diagSet